src/HOL/Number_Theory/Primes.thy
 author paulson Sun Feb 02 19:15:25 2014 +0000 (2014-02-02) changeset 55242 413ec965f95d parent 55238 7ddb889e23bd child 55337 5d45fb978d5a permissions -rw-r--r--
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
```     1 (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
```
```     2                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
```
```     3
```
```     4
```
```     5 This file deals with properties of primes. Definitions and lemmas are
```
```     6 proved uniformly for the natural numbers and integers.
```
```     7
```
```     8 This file combines and revises a number of prior developments.
```
```     9
```
```    10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
```
```    11 and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
```
```    12 gcd, lcm, and prime for the natural numbers.
```
```    13
```
```    14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
```
```    15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
```
```    16 another extension of the notions to the integers, and added a number
```
```    17 of results to "Primes" and "GCD". IntPrimes also defined and developed
```
```    18 the congruence relations on the integers. The notion was extended to
```
```    19 the natural numbers by Chaieb.
```
```    20
```
```    21 Jeremy Avigad combined all of these, made everything uniform for the
```
```    22 natural numbers and the integers, and added a number of new theorems.
```
```    23
```
```    24 Tobias Nipkow cleaned up a lot.
```
```    25 *)
```
```    26
```
```    27
```
```    28 header {* Primes *}
```
```    29
```
```    30 theory Primes
```
```    31 imports "~~/src/HOL/GCD"
```
```    32 begin
```
```    33
```
```    34 declare One_nat_def [simp]
```
```    35 declare [[coercion int]]
```
```    36 declare [[coercion_enabled]]
```
```    37
```
```    38 definition prime :: "nat \<Rightarrow> bool"
```
```    39   where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
```
```    40
```
```    41 lemmas prime_nat_def = prime_def
```
```    42
```
```    43
```
```    44 subsection {* Primes *}
```
```    45
```
```    46 lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
```
```    47   apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
```
```    48   apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
```
```    49   done
```
```    50
```
```    51 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
```
```    52
```
```    53 lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
```
```    54   unfolding prime_nat_def by auto
```
```    55
```
```    56 lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
```
```    57   unfolding prime_nat_def by auto
```
```    58
```
```    59 lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
```
```    60   unfolding prime_nat_def by auto
```
```    61
```
```    62 lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
```
```    63   unfolding prime_nat_def by auto
```
```    64
```
```    65 lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
```
```    66   unfolding prime_nat_def by auto
```
```    67
```
```    68 lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
```
```    69   unfolding prime_nat_def by auto
```
```    70
```
```    71 lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
```
```    72   apply (unfold prime_nat_def)
```
```    73   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
```
```    74   done
```
```    75
```
```    76 lemma prime_int_altdef:
```
```    77   "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
```
```    78     m = 1 \<or> m = p))"
```
```    79   apply (simp add: prime_def)
```
```    80   apply (auto simp add: )
```
```    81   apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
```
```    82   apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
```
```    83   done
```
```    84
```
```    85 lemma prime_imp_coprime_int:
```
```    86   fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
```
```    87   apply (unfold prime_int_altdef)
```
```    88   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
```
```    89   done
```
```    90
```
```    91 lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
```
```    92   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
```
```    93
```
```    94 lemma prime_dvd_mult_int:
```
```    95   fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
```
```    96   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
```
```    97
```
```    98 lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
```
```    99     p dvd m * n = (p dvd m \<or> p dvd n)"
```
```   100   by (rule iffI, rule prime_dvd_mult_nat, auto)
```
```   101
```
```   102 lemma prime_dvd_mult_eq_int [simp]:
```
```   103   fixes n::int
```
```   104   shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
```
```   105   by (rule iffI, rule prime_dvd_mult_int, auto)
```
```   106
```
```   107 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
```
```   108     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
```
```   109   unfolding prime_nat_def dvd_def apply auto
```
```   110   by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
```
```   111       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
```
```   112
```
```   113 lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
```
```   114   by (induct n) auto
```
```   115
```
```   116 lemma prime_dvd_power_int:
```
```   117   fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
```
```   118   by (induct n) auto
```
```   119
```
```   120 lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
```
```   121     p dvd x^n \<longleftrightarrow> p dvd x"
```
```   122   by (cases n) (auto elim: prime_dvd_power_nat)
```
```   123
```
```   124 lemma prime_dvd_power_int_iff:
```
```   125   fixes x::int
```
```   126   shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
```
```   127   by (cases n) (auto elim: prime_dvd_power_int)
```
```   128
```
```   129
```
```   130 subsubsection {* Make prime naively executable *}
```
```   131
```
```   132 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
```
```   133   by (simp add: prime_nat_def)
```
```   134
```
```   135 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
```
```   136   by (simp add: prime_nat_def)
```
```   137
```
```   138 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
```
```   139   by (simp add: prime_nat_def)
```
```   140
```
```   141 lemma prime_nat_code [code]:
```
```   142     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
```
```   143   apply (simp add: Ball_def)
```
```   144   apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
```
```   145   done
```
```   146
```
```   147 lemma prime_nat_simp:
```
```   148     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
```
```   149   by (auto simp add: prime_nat_code)
```
```   150
```
```   151 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
```
```   152
```
```   153 lemma two_is_prime_nat [simp]: "prime (2::nat)"
```
```   154   by simp
```
```   155
```
```   156 text{* A bit of regression testing: *}
```
```   157
```
```   158 lemma "prime(97::nat)" by simp
```
```   159 lemma "prime(997::nat)" by eval
```
```   160
```
```   161
```
```   162 lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
```
```   163   by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
```
```   164
```
```   165 lemma prime_imp_power_coprime_int:
```
```   166   fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
```
```   167   by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
```
```   168
```
```   169 lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
```
```   170   by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
```
```   171
```
```   172 lemma primes_imp_powers_coprime_nat:
```
```   173     "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
```
```   174   by (rule coprime_exp2_nat, rule primes_coprime_nat)
```
```   175
```
```   176 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
```
```   177   apply (induct n rule: nat_less_induct)
```
```   178   apply (case_tac "n = 0")
```
```   179   using two_is_prime_nat
```
```   180   apply blast
```
```   181   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
```
```   182     nat_dvd_not_less neq0_conv prime_nat_def)
```
```   183   done
```
```   184
```
```   185 text {* One property of coprimality is easier to prove via prime factors. *}
```
```   186
```
```   187 lemma prime_divprod_pow_nat:
```
```   188   assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
```
```   189   shows "p^n dvd a \<or> p^n dvd b"
```
```   190 proof-
```
```   191   { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
```
```   192       apply (cases "n=0", simp_all)
```
```   193       apply (cases "a=1", simp_all)
```
```   194       done }
```
```   195   moreover
```
```   196   { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
```
```   197     then obtain m where m: "n = Suc m" by (cases n) auto
```
```   198     from n have "p dvd p^n" apply (intro dvd_power) apply auto done
```
```   199     also note pab
```
```   200     finally have pab': "p dvd a * b".
```
```   201     from prime_dvd_mult_nat[OF p pab']
```
```   202     have "p dvd a \<or> p dvd b" .
```
```   203     moreover
```
```   204     { assume pa: "p dvd a"
```
```   205       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
```
```   206       with p have "coprime b p"
```
```   207         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
```
```   208       then have pnb: "coprime (p^n) b"
```
```   209         by (subst gcd_commute_nat, rule coprime_exp_nat)
```
```   210       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
```
```   211     moreover
```
```   212     { assume pb: "p dvd b"
```
```   213       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
```
```   214       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
```
```   215         by auto
```
```   216       with p have "coprime a p"
```
```   217         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
```
```   218       then have pna: "coprime (p^n) a"
```
```   219         by (subst gcd_commute_nat, rule coprime_exp_nat)
```
```   220       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
```
```   221     ultimately have ?thesis by blast }
```
```   222   ultimately show ?thesis by blast
```
```   223 qed
```
```   224
```
```   225
```
```   226 subsection {* Infinitely many primes *}
```
```   227
```
```   228 lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
```
```   229 proof-
```
```   230   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
```
```   231   from prime_factor_nat [OF f1]
```
```   232   obtain p where "prime p" and "p dvd fact n + 1" by auto
```
```   233   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
```
```   234   { assume "p \<le> n"
```
```   235     from `prime p` have "p \<ge> 1"
```
```   236       by (cases p, simp_all)
```
```   237     with `p <= n` have "p dvd fact n"
```
```   238       by (intro dvd_fact_nat)
```
```   239     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
```
```   240       by (rule dvd_diff_nat)
```
```   241     then have "p dvd 1" by simp
```
```   242     then have "p <= 1" by auto
```
```   243     moreover from `prime p` have "p > 1" by auto
```
```   244     ultimately have False by auto}
```
```   245   then have "n < p" by presburger
```
```   246   with `prime p` and `p <= fact n + 1` show ?thesis by auto
```
```   247 qed
```
```   248
```
```   249 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
```
```   250   using next_prime_bound by auto
```
```   251
```
```   252 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
```
```   253 proof
```
```   254   assume "finite {(p::nat). prime p}"
```
```   255   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
```
```   256     by auto
```
```   257   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
```
```   258     by auto
```
```   259   with bigger_prime [of b] show False
```
```   260     by auto
```
```   261 qed
```
```   262
```
```   263 subsection{*Powers of Primes*}
```
```   264
```
```   265 text{*Versions for type nat only*}
```
```   266
```
```   267 lemma prime_product:
```
```   268   fixes p::nat
```
```   269   assumes "prime (p * q)"
```
```   270   shows "p = 1 \<or> q = 1"
```
```   271 proof -
```
```   272   from assms have
```
```   273     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
```
```   274     unfolding prime_nat_def by auto
```
```   275   from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
```
```   276   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
```
```   277   have "p dvd p * q" by simp
```
```   278   then have "p = 1 \<or> p = p * q" by (rule P)
```
```   279   then show ?thesis by (simp add: Q)
```
```   280 qed
```
```   281
```
```   282 lemma prime_exp:
```
```   283   fixes p::nat
```
```   284   shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
```
```   285 proof(induct n)
```
```   286   case 0 thus ?case by simp
```
```   287 next
```
```   288   case (Suc n)
```
```   289   {assume "p = 0" hence ?case by simp}
```
```   290   moreover
```
```   291   {assume "p=1" hence ?case by simp}
```
```   292   moreover
```
```   293   {assume p: "p \<noteq> 0" "p\<noteq>1"
```
```   294     {assume pp: "prime (p^Suc n)"
```
```   295       hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
```
```   296       with p have n: "n = 0"
```
```   297         by (metis One_nat_def nat_power_eq_Suc_0_iff)
```
```   298       with pp have "prime p \<and> Suc n = 1" by simp}
```
```   299     moreover
```
```   300     {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
```
```   301     ultimately have ?case by blast}
```
```   302   ultimately show ?case by blast
```
```   303 qed
```
```   304
```
```   305 lemma prime_power_mult:
```
```   306   fixes p::nat
```
```   307   assumes p: "prime p" and xy: "x * y = p ^ k"
```
```   308   shows "\<exists>i j. x = p ^i \<and> y = p^ j"
```
```   309 using xy
```
```   310 proof(induct k arbitrary: x y)
```
```   311   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
```
```   312 next
```
```   313   case (Suc k x y)
```
```   314   from Suc.prems have pxy: "p dvd x*y" by auto
```
```   315   from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
```
```   316   from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
```
```   317   {assume px: "p dvd x"
```
```   318     then obtain d where d: "x = p*d" unfolding dvd_def by blast
```
```   319     from Suc.prems d  have "p*d*y = p^Suc k" by simp
```
```   320     hence th: "d*y = p^k" using p0 by simp
```
```   321     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
```
```   322     with d have "x = p^Suc i" by simp
```
```   323     with ij(2) have ?case by blast}
```
```   324   moreover
```
```   325   {assume px: "p dvd y"
```
```   326     then obtain d where d: "y = p*d" unfolding dvd_def by blast
```
```   327     from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult_commute)
```
```   328     hence th: "d*x = p^k" using p0 by simp
```
```   329     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
```
```   330     with d have "y = p^Suc i" by simp
```
```   331     with ij(2) have ?case by blast}
```
```   332   ultimately show ?case  using pxyc by blast
```
```   333 qed
```
```   334
```
```   335 lemma prime_power_exp:
```
```   336   fixes p::nat
```
```   337   assumes p: "prime p" and n: "n \<noteq> 0"
```
```   338     and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
```
```   339   using n xn
```
```   340 proof(induct n arbitrary: k)
```
```   341   case 0 thus ?case by simp
```
```   342 next
```
```   343   case (Suc n k) hence th: "x*x^n = p^k" by simp
```
```   344   {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
```
```   345   moreover
```
```   346   {assume n: "n \<noteq> 0"
```
```   347     from prime_power_mult[OF p th]
```
```   348     obtain i j where ij: "x = p^i" "x^n = p^j"by blast
```
```   349     from Suc.hyps[OF n ij(2)] have ?case .}
```
```   350   ultimately show ?case by blast
```
```   351 qed
```
```   352
```
```   353 lemma divides_primepow:
```
```   354   fixes p::nat
```
```   355   assumes p: "prime p"
```
```   356   shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
```
```   357 proof
```
```   358   assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
```
```   359     unfolding dvd_def  apply (auto simp add: mult_commute) by blast
```
```   360   from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
```
```   361   from e ij have "p^(i + j) = p^k" by (simp add: power_add)
```
```   362   hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
```
```   363   hence "i \<le> k" by arith
```
```   364   with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
```
```   365 next
```
```   366   {fix i assume H: "i \<le> k" "d = p^i"
```
```   367     then obtain j where j: "k = i + j"
```
```   368       by (metis le_add_diff_inverse)
```
```   369     hence "p^k = p^j*d" using H(2) by (simp add: power_add)
```
```   370     hence "d dvd p^k" unfolding dvd_def by auto}
```
```   371   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
```
```   372 qed
```
```   373
```
```   374 subsection {*Chinese Remainder Theorem Variants*}
```
```   375
```
```   376 lemma bezout_gcd_nat:
```
```   377   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
```
```   378   using bezout_nat[of a b]
```
```   379 by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute
```
```   380   gcd_nat.right_neutral mult_0)
```
```   381
```
```   382 lemma gcd_bezout_sum_nat:
```
```   383   fixes a::nat
```
```   384   assumes "a * x + b * y = d"
```
```   385   shows "gcd a b dvd d"
```
```   386 proof-
```
```   387   let ?g = "gcd a b"
```
```   388     have dv: "?g dvd a*x" "?g dvd b * y"
```
```   389       by simp_all
```
```   390     from dvd_add[OF dv] assms
```
```   391     show ?thesis by auto
```
```   392 qed
```
```   393
```
```   394
```
```   395 text {* A binary form of the Chinese Remainder Theorem. *}
```
```   396
```
```   397 lemma chinese_remainder:
```
```   398   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
```
```   399   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
```
```   400 proof-
```
```   401   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
```
```   402   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
```
```   403     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
```
```   404   then have d12: "d1 = 1" "d2 =1"
```
```   405     by (metis ab coprime_nat)+
```
```   406   let ?x = "v * a * x1 + u * b * x2"
```
```   407   let ?q1 = "v * x1 + u * y2"
```
```   408   let ?q2 = "v * y1 + u * x2"
```
```   409   from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
```
```   410   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
```
```   411     apply (auto simp add: algebra_simps)
```
```   412     apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
```
```   413     done
```
```   414   thus ?thesis by blast
```
```   415 qed
```
```   416
```
```   417 text {* Primality *}
```
```   418
```
```   419 lemma coprime_bezout_strong:
```
```   420   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
```
```   421   shows "\<exists>x y. a * x = b * y + 1"
```
```   422 by (metis assms bezout_nat gcd_nat.left_neutral)
```
```   423
```
```   424 lemma bezout_prime:
```
```   425   assumes p: "prime p" and pa: "\<not> p dvd a"
```
```   426   shows "\<exists>x y. a*x = Suc (p*y)"
```
```   427 proof-
```
```   428   have ap: "coprime a p"
```
```   429     by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
```
```   430   from coprime_bezout_strong[OF ap] show ?thesis
```
```   431     by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
```
```   432 qed
```
```   433
```
```   434 end
```