2013-08-19から1日間の記事一覧
let lem2pn = GSYM(SIMP_RULE[REAL_POW_ONE;REAL_MUL_RID;REAL_ARITH`&1 + &1 = &2`](SPECL[`n:num`;`&1`;`&1`]REAL_BINOMIAL_THEOREM));; g`sum (0..m) (\k. &(binom (n,k))) <= sum (0..n) (\k. &(binom (n,k)))`;; e(DISJ_CASES_TAC(ARITH_RULE`m <= n \/…