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