equal
deleted
inserted
replaced
28 Goal "i^n = 0 ==> i = (0::nat)"; |
28 Goal "i^n = 0 ==> i = (0::nat)"; |
29 by (etac contrapos_pp 1); |
29 by (etac contrapos_pp 1); |
30 by Auto_tac; |
30 by Auto_tac; |
31 qed "power_eq_0D"; |
31 qed "power_eq_0D"; |
32 |
32 |
33 Goal "!!i::nat. 1 <= i ==> 1 <= i^n"; |
33 Goal "!!i::nat. 1 <= i ==> 1' <= i^n"; |
34 by (induct_tac "n" 1); |
34 by (induct_tac "n" 1); |
35 by Auto_tac; |
35 by Auto_tac; |
36 qed "one_le_power"; |
36 qed "one_le_power"; |
37 Addsimps [one_le_power]; |
37 Addsimps [one_le_power]; |
38 |
38 |
118 by (induct_tac "n" 1); |
118 by (induct_tac "n" 1); |
119 by (ALLGOALS Asm_simp_tac); |
119 by (ALLGOALS Asm_simp_tac); |
120 qed "binomial_Suc_n"; |
120 qed "binomial_Suc_n"; |
121 Addsimps [binomial_Suc_n]; |
121 Addsimps [binomial_Suc_n]; |
122 |
122 |
123 Goal "(n choose 1) = n"; |
123 Goal "(n choose 1') = n"; |
124 by (induct_tac "n" 1); |
124 by (induct_tac "n" 1); |
125 by (ALLGOALS Asm_simp_tac); |
125 by (ALLGOALS Asm_simp_tac); |
126 qed "binomial_1"; |
126 qed "binomial_1"; |
127 Addsimps [binomial_1]; |
127 Addsimps [binomial_1]; |
128 |
128 |