src/HOL/Old_Number_Theory/Gauss.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44766 d4d33a4d7548
child 46756 faf62905cd53
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Title:      HOL/Old_Number_Theory/Gauss.thy
     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3 *)
     4 
     5 header {* Gauss' Lemma *}
     6 
     7 theory Gauss
     8 imports Euler
     9 begin
    10 
    11 locale GAUSS =
    12   fixes p :: "int"
    13   fixes a :: "int"
    14 
    15   assumes p_prime: "zprime p"
    16   assumes p_g_2: "2 < p"
    17   assumes p_a_relprime: "~[a = 0](mod p)"
    18   assumes a_nonzero:    "0 < a"
    19 begin
    20 
    21 definition "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
    22 definition "B = (%x. x * a) ` A"
    23 definition "C = StandardRes p ` B"
    24 definition "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
    25 definition "E = C \<inter> {x. ((p - 1) div 2) < x}"
    26 definition "F = (%x. (p - x)) ` E"
    27 
    28 
    29 subsection {* Basic properties of p *}
    30 
    31 lemma p_odd: "p \<in> zOdd"
    32   by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
    33 
    34 lemma p_g_0: "0 < p"
    35   using p_g_2 by auto
    36 
    37 lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
    38   using ListMem.insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
    39 
    40 lemma p_minus_one_l: "(p - 1) div 2 < p"
    41 proof -
    42   have "(p - 1) div 2 \<le> (p - 1) div 1"
    43     by (rule zdiv_mono2) (auto simp add: p_g_0)
    44   also have "\<dots> = p - 1" by simp
    45   finally show ?thesis by simp
    46 qed
    47 
    48 lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
    49   using div_mult_self1_is_id [of 2 "p - 1"] by auto
    50 
    51 
    52 lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
    53   apply (frule odd_minus_one_even)
    54   apply (simp add: zEven_def)
    55   apply (subgoal_tac "2 \<noteq> 0")
    56   apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
    57   apply (auto simp add: even_div_2_prop2)
    58   done
    59 
    60 
    61 lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
    62   apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
    63   apply (frule zodd_imp_zdiv_eq, auto)
    64   done
    65 
    66 
    67 subsection {* Basic Properties of the Gauss Sets *}
    68 
    69 lemma finite_A: "finite (A)"
    70   apply (auto simp add: A_def)
    71   apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
    72   apply (auto simp add: bdd_int_set_l_finite finite_subset)
    73   done
    74 
    75 lemma finite_B: "finite (B)"
    76 by (auto simp add: B_def finite_A)
    77 
    78 lemma finite_C: "finite (C)"
    79 by (auto simp add: C_def finite_B)
    80 
    81 lemma finite_D: "finite (D)"
    82 by (auto simp add: D_def finite_C)
    83 
    84 lemma finite_E: "finite (E)"
    85 by (auto simp add: E_def finite_C)
    86 
    87 lemma finite_F: "finite (F)"
    88 by (auto simp add: F_def finite_E)
    89 
    90 lemma C_eq: "C = D \<union> E"
    91 by (auto simp add: C_def D_def E_def)
    92 
    93 lemma A_card_eq: "card A = nat ((p - 1) div 2)"
    94   apply (auto simp add: A_def)
    95   apply (insert int_nat)
    96   apply (erule subst)
    97   apply (auto simp add: card_bdd_int_set_l_le)
    98   done
    99 
   100 lemma inj_on_xa_A: "inj_on (%x. x * a) A"
   101   using a_nonzero by (simp add: A_def inj_on_def)
   102 
   103 lemma A_res: "ResSet p A"
   104   apply (auto simp add: A_def ResSet_def)
   105   apply (rule_tac m = p in zcong_less_eq)
   106   apply (insert p_g_2, auto)
   107   done
   108 
   109 lemma B_res: "ResSet p B"
   110   apply (insert p_g_2 p_a_relprime p_minus_one_l)
   111   apply (auto simp add: B_def)
   112   apply (rule ResSet_image)
   113   apply (auto simp add: A_res)
   114   apply (auto simp add: A_def)
   115 proof -
   116   fix x fix y
   117   assume a: "[x * a = y * a] (mod p)"
   118   assume b: "0 < x"
   119   assume c: "x \<le> (p - 1) div 2"
   120   assume d: "0 < y"
   121   assume e: "y \<le> (p - 1) div 2"
   122   from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
   123   have "[x = y](mod p)"
   124     by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
   125   with zcong_less_eq [of x y p] p_minus_one_l
   126       order_le_less_trans [of x "(p - 1) div 2" p]
   127       order_le_less_trans [of y "(p - 1) div 2" p] show "x = y"
   128     by (simp add: b c d e p_minus_one_l p_g_0)
   129 qed
   130 
   131 lemma SR_B_inj: "inj_on (StandardRes p) B"
   132   apply (auto simp add: B_def StandardRes_def inj_on_def A_def)
   133 proof -
   134   fix x fix y
   135   assume a: "x * a mod p = y * a mod p"
   136   assume b: "0 < x"
   137   assume c: "x \<le> (p - 1) div 2"
   138   assume d: "0 < y"
   139   assume e: "y \<le> (p - 1) div 2"
   140   assume f: "x \<noteq> y"
   141   from a have "[x * a = y * a](mod p)"
   142     by (simp add: zcong_zmod_eq p_g_0)
   143   with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
   144   have "[x = y](mod p)"
   145     by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
   146   with zcong_less_eq [of x y p] p_minus_one_l
   147     order_le_less_trans [of x "(p - 1) div 2" p]
   148     order_le_less_trans [of y "(p - 1) div 2" p] have "x = y"
   149     by (simp add: b c d e p_minus_one_l p_g_0)
   150   then have False
   151     by (simp add: f)
   152   then show "a = 0"
   153     by simp
   154 qed
   155 
   156 lemma inj_on_pminusx_E: "inj_on (%x. p - x) E"
   157   apply (auto simp add: E_def C_def B_def A_def)
   158   apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI)
   159   apply auto
   160   done
   161 
   162 lemma A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
   163   apply (auto simp add: A_def)
   164   apply (frule_tac m = p in zcong_not_zero)
   165   apply (insert p_minus_one_l)
   166   apply auto
   167   done
   168 
   169 lemma A_greater_zero: "x \<in> A ==> 0 < x"
   170   by (auto simp add: A_def)
   171 
   172 lemma B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
   173   apply (auto simp add: B_def)
   174   apply (frule A_ncong_p)
   175   apply (insert p_a_relprime p_prime a_nonzero)
   176   apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
   177   apply (auto simp add: A_greater_zero)
   178   done
   179 
   180 lemma B_greater_zero: "x \<in> B ==> 0 < x"
   181   using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
   182 
   183 lemma C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
   184   apply (auto simp add: C_def)
   185   apply (frule B_ncong_p)
   186   apply (subgoal_tac "[x = StandardRes p x](mod p)")
   187   defer apply (simp add: StandardRes_prop1)
   188   apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
   189   apply auto
   190   done
   191 
   192 lemma C_greater_zero: "y \<in> C ==> 0 < y"
   193   apply (auto simp add: C_def)
   194 proof -
   195   fix x
   196   assume a: "x \<in> B"
   197   from p_g_0 have "0 \<le> StandardRes p x"
   198     by (simp add: StandardRes_lbound)
   199   moreover have "~[x = 0] (mod p)"
   200     by (simp add: a B_ncong_p)
   201   then have "StandardRes p x \<noteq> 0"
   202     by (simp add: StandardRes_prop3)
   203   ultimately show "0 < StandardRes p x"
   204     by (simp add: order_le_less)
   205 qed
   206 
   207 lemma D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
   208   by (auto simp add: D_def C_ncong_p)
   209 
   210 lemma E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
   211   by (auto simp add: E_def C_ncong_p)
   212 
   213 lemma F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
   214   apply (auto simp add: F_def)
   215 proof -
   216   fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
   217   from E_ncong_p have "~[x = 0] (mod p)"
   218     by (simp add: a)
   219   moreover from a have "0 < x"
   220     by (simp add: a E_def C_greater_zero)
   221   moreover from a have "x < p"
   222     by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
   223   ultimately have "~[p - x = 0] (mod p)"
   224     by (simp add: zcong_not_zero)
   225   from this show False by (simp add: b)
   226 qed
   227 
   228 lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   229   apply (auto simp add: F_def E_def)
   230   apply (insert p_g_0)
   231   apply (frule_tac x = xa in StandardRes_ubound)
   232   apply (frule_tac x = x in StandardRes_ubound)
   233   apply (subgoal_tac "xa = StandardRes p xa")
   234   apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
   235 proof -
   236   from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have
   237     "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)"
   238     by simp
   239   with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
   240       ==> p - StandardRes p x \<le> (p - 1) div 2"
   241     by simp
   242 qed
   243 
   244 lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   245   by (auto simp add: D_def C_greater_zero)
   246 
   247 lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"
   248   by (auto simp add: F_def E_def D_def C_def B_def A_def)
   249 
   250 lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}"
   251   by (auto simp add: D_def C_def B_def A_def)
   252 
   253 lemma D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   254   by (auto simp add: D_eq)
   255 
   256 lemma F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   257   apply (auto simp add: F_eq A_def)
   258 proof -
   259   fix y
   260   assume "(p - 1) div 2 < StandardRes p (y * a)"
   261   then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)"
   262     by arith
   263   also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"
   264     by auto
   265   also have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1"
   266     by arith
   267   finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2"
   268     using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
   269 qed
   270 
   271 lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1"
   272   using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
   273 
   274 lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
   275 by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
   276 
   277 
   278 subsection {* Relationships Between Gauss Sets *}
   279 
   280 lemma B_card_eq_A: "card B = card A"
   281   using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
   282 
   283 lemma B_card_eq: "card B = nat ((p - 1) div 2)"
   284   by (simp add: B_card_eq_A A_card_eq)
   285 
   286 lemma F_card_eq_E: "card F = card E"
   287   using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
   288 
   289 lemma C_card_eq_B: "card C = card B"
   290   apply (insert finite_B)
   291   apply (subgoal_tac "inj_on (StandardRes p) B")
   292   apply (simp add: B_def C_def card_image)
   293   apply (rule StandardRes_inj_on_ResSet)
   294   apply (simp add: B_res)
   295   done
   296 
   297 lemma D_E_disj: "D \<inter> E = {}"
   298   by (auto simp add: D_def E_def)
   299 
   300 lemma C_card_eq_D_plus_E: "card C = card D + card E"
   301   by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
   302 
   303 lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
   304   apply (insert D_E_disj finite_D finite_E C_eq)
   305   apply (frule setprod_Un_disjoint [of D E id])
   306   apply auto
   307   done
   308 
   309 lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   310   apply (auto simp add: C_def)
   311   apply (insert finite_B SR_B_inj)
   312   apply (frule_tac f = "StandardRes p" in setprod_reindex_id [symmetric], auto)
   313   apply (rule setprod_same_function_zcong)
   314   apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   315   done
   316 
   317 lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
   318   apply (rule Un_least)
   319   apply (auto simp add: A_def F_subset D_subset)
   320   done
   321 
   322 lemma F_D_disj: "(F \<inter> D) = {}"
   323   apply (simp add: F_eq D_eq)
   324   apply (auto simp add: F_eq D_eq)
   325 proof -
   326   fix y fix ya
   327   assume "p - StandardRes p (y * a) = StandardRes p (ya * a)"
   328   then have "p = StandardRes p (y * a) + StandardRes p (ya * a)"
   329     by arith
   330   moreover have "p dvd p"
   331     by auto
   332   ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))"
   333     by auto
   334   then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)"
   335     by (auto simp add: zcong_def)
   336   have "[y * a = StandardRes p (y * a)] (mod p)"
   337     by (simp only: zcong_sym StandardRes_prop1)
   338   moreover have "[ya * a = StandardRes p (ya * a)] (mod p)"
   339     by (simp only: zcong_sym StandardRes_prop1)
   340   ultimately have "[y * a + ya * a =
   341     StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)"
   342     by (rule zcong_zadd)
   343   with a have "[y * a + ya * a = 0] (mod p)"
   344     apply (elim zcong_trans)
   345     by (simp only: zcong_refl)
   346   also have "y * a + ya * a = a * (y + ya)"
   347     by (simp add: right_distrib mult_commute)
   348   finally have "[a * (y + ya) = 0] (mod p)" .
   349   with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
   350     p_a_relprime
   351   have a: "[y + ya = 0] (mod p)"
   352     by auto
   353   assume b: "y \<in> A" and c: "ya: A"
   354   with A_def have "0 < y + ya"
   355     by auto
   356   moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2"
   357     by auto
   358   moreover from b c p_eq2 A_def have "y + ya < p"
   359     by auto
   360   ultimately show False
   361     apply simp
   362     apply (frule_tac m = p in zcong_not_zero)
   363     apply (auto simp add: a)
   364     done
   365 qed
   366 
   367 lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
   368 proof -
   369   have "card (F \<union> D) = card E + card D"
   370     by (auto simp add: finite_F finite_D F_D_disj
   371       card_Un_disjoint F_card_eq_E)
   372   then have "card (F \<union> D) = card C"
   373     by (simp add: C_card_eq_D_plus_E)
   374   from this show "card (F \<union> D) = nat ((p - 1) div 2)"
   375     by (simp add: C_card_eq_B B_card_eq)
   376 qed
   377 
   378 lemma F_Un_D_eq_A: "F \<union> D = A"
   379   using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
   380 
   381 lemma prod_D_F_eq_prod_A:
   382     "(setprod id D) * (setprod id F) = setprod id A"
   383   apply (insert F_D_disj finite_D finite_F)
   384   apply (frule setprod_Un_disjoint [of F D id])
   385   apply (auto simp add: F_Un_D_eq_A)
   386   done
   387 
   388 lemma prod_F_zcong:
   389   "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
   390 proof -
   391   have "setprod id F = setprod id (op - p ` E)"
   392     by (auto simp add: F_def)
   393   then have "setprod id F = setprod (op - p) E"
   394     apply simp
   395     apply (insert finite_E inj_on_pminusx_E)
   396     apply (frule_tac f = "op - p" in setprod_reindex_id, auto)
   397     done
   398   then have one:
   399     "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
   400     apply simp
   401     apply (insert p_g_0 finite_E StandardRes_prod)
   402     by (auto)
   403   moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
   404     apply clarify
   405     apply (insert zcong_id [of p])
   406     apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
   407     done
   408   moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
   409     apply clarify
   410     apply (simp add: StandardRes_prop1 zcong_sym)
   411     done
   412   moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
   413     apply clarify
   414     apply (insert a b)
   415     apply (rule_tac b = "p - x" in zcong_trans, auto)
   416     done
   417   ultimately have c:
   418     "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
   419     apply simp
   420     using finite_E p_g_0
   421       setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
   422     by auto
   423   then have two: "[setprod id F = setprod (uminus) E](mod p)"
   424     apply (insert one c)
   425     apply (rule zcong_trans [of "setprod id F"
   426                                "setprod (StandardRes p o op - p) E" p
   427                                "setprod uminus E"], auto)
   428     done
   429   also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
   430     using finite_E by (induct set: finite) auto
   431   then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   432     by (simp add: mult_commute)
   433   with two show ?thesis
   434     by simp
   435 qed
   436 
   437 
   438 subsection {* Gauss' Lemma *}
   439 
   440 lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
   441   by (auto simp add: finite_E neg_one_special)
   442 
   443 theorem pre_gauss_lemma:
   444   "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   445 proof -
   446   have "[setprod id A = setprod id F * setprod id D](mod p)"
   447     by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong)
   448   then have "[setprod id A = ((-1)^(card E) * setprod id E) *
   449       setprod id D] (mod p)"
   450     apply (rule zcong_trans)
   451     apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod_cong)
   452     done
   453   then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   454     apply (rule zcong_trans)
   455     apply (insert C_prod_eq_D_times_E, erule subst)
   456     apply (subst mult_assoc, auto)
   457     done
   458   then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   459     apply (rule zcong_trans)
   460     apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod_cong)
   461     done
   462   then have "[setprod id A = ((-1)^(card E) *
   463     (setprod id ((%x. x * a) ` A)))] (mod p)"
   464     by (simp add: B_def)
   465   then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
   466     (mod p)"
   467     by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
   468   moreover have "setprod (%x. x * a) A =
   469     setprod (%x. a) A * setprod id A"
   470     using finite_A by (induct set: finite) auto
   471   ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
   472     setprod id A))] (mod p)"
   473     by simp
   474   then have "[setprod id A = ((-1)^(card E) * a^(card A) *
   475       setprod id A)](mod p)"
   476     apply (rule zcong_trans)
   477     apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult_assoc)
   478     done
   479   then have a: "[setprod id A * (-1)^(card E) =
   480       ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
   481     by (rule zcong_scalar)
   482   then have "[setprod id A * (-1)^(card E) = setprod id A *
   483       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   484     apply (rule zcong_trans)
   485     apply (simp add: a mult_commute mult_left_commute)
   486     done
   487   then have "[setprod id A * (-1)^(card E) = setprod id A *
   488       a^(card A)](mod p)"
   489     apply (rule zcong_trans)
   490     apply (simp add: aux cong del:setprod_cong)
   491     done
   492   with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
   493       p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   494     by (simp add: order_less_imp_le)
   495   from this show ?thesis
   496     by (simp add: A_card_eq zcong_sym)
   497 qed
   498 
   499 theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   500 proof -
   501   from Euler_Criterion p_prime p_g_2 have
   502       "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   503     by auto
   504   moreover note pre_gauss_lemma
   505   ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
   506     by (rule zcong_trans)
   507   moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
   508     by (auto simp add: Legendre_def)
   509   moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
   510     by (rule neg_one_power)
   511   ultimately show ?thesis
   512     by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
   513 qed
   514 
   515 end
   516 
   517 end