src/HOL/Number_Theory/Primes.thy
 changeset 62481 b5d8e57826df parent 62429 25271ff79171 child 63534 523b488b15c9
```     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 01 10:32:55 2016 +0100
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Mar 01 10:36:19 2016 +0100
1.3 @@ -96,11 +96,11 @@
1.4    shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
1.5    by (rule iffI, rule prime_dvd_mult_int, auto)
1.6
1.7 -lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
1.8 -    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1.9 -  unfolding prime_def dvd_def apply auto
1.10 -  by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
1.11 -      n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
1.12 +lemma not_prime_eq_prod_nat:
1.13 +  "1 < n \<Longrightarrow> \<not> prime n \<Longrightarrow>
1.14 +    \<exists>m k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
1.15 +  unfolding prime_def dvd_def apply (auto simp add: ac_simps)
1.16 +  by (metis Suc_lessD Suc_lessI n_less_m_mult_n n_less_n_mult_m nat_0_less_mult_iff)
1.17
1.18  lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
1.19    by (induct n) auto
```