equal
deleted
inserted
replaced
38 |
38 |
39 Goal "!!i::nat. 1 < i ==> !m. (i^n = i^m) = (n=m)"; |
39 Goal "!!i::nat. 1 < i ==> !m. (i^n = i^m) = (n=m)"; |
40 by (induct_tac "n" 1); |
40 by (induct_tac "n" 1); |
41 by Auto_tac; |
41 by Auto_tac; |
42 by (ALLGOALS (case_tac "m")); |
42 by (ALLGOALS (case_tac "m")); |
|
43 by (Simp_tac 1); |
43 by Auto_tac; |
44 by Auto_tac; |
44 qed_spec_mp "power_inject"; |
45 qed_spec_mp "power_inject"; |
45 Addsimps [power_inject]; |
46 Addsimps [power_inject]; |
46 |
47 |
47 Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n"; |
48 Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n"; |