equal
deleted
inserted
replaced
183 |
183 |
184 lemma two_is_prime: "2 \<in> prime" |
184 lemma two_is_prime: "2 \<in> prime" |
185 apply (auto simp add: prime_def) |
185 apply (auto simp add: prime_def) |
186 apply (case_tac m) |
186 apply (case_tac m) |
187 apply (auto dest!: dvd_imp_le) |
187 apply (auto dest!: dvd_imp_le) |
188 apply arith |
|
189 done |
188 done |
190 |
189 |
191 text {* |
190 text {* |
192 This theorem leads immediately to a proof of the uniqueness of |
191 This theorem leads immediately to a proof of the uniqueness of |
193 factorization. If @{term p} divides a product of primes then it is |
192 factorization. If @{term p} divides a product of primes then it is |