a is unbounded

euler.v

@@ -17,42 +17,43 @@ apply/eqP; elim/big_rec2: _ => // i m n _ /eqP nEm.
 by rewrite modnMml -modnMmr nEm modnMmr.
 Qed.
 
-Definition res_quad p a := has (fun i => (i * i) %% p == a) (iota 0 p).
+Definition res_quad p a := has (fun i => i * i == a %[mod p]) (iota 0 p).
 
 Compute res_quad 7 4.
 
 Lemma res_quadP a p : 
-  reflect (exists i : 'I_p, (i * i) %% p = a) (res_quad p a).
+  reflect (exists i : 'I_p, i * i = a %[mod p]) (res_quad p a).
 Proof. 
 apply: (iffP hasP) => [[x /[!mem_iota] [/andP[_ xLp] /eqP xxE]]|[x xxE]].
   by exists (Ordinal xLp).
 by exists (val x); [rewrite mem_iota /= | apply/eqP].
 Qed.
 
 Lemma res_quadPn a p : 
-  reflect (forall i : 'I_p, (i * i) %% p != a) (~~ (res_quad p a)).
+  reflect (forall i : 'I_p, i * i != a %[mod p]) (~~ (res_quad p a)).
 Proof.
 apply: (iffP hasPn) => [xxE i| xxE i /[!mem_iota] /= iI].
   by apply: xxE; rewrite mem_iota /=.
 by apply: (xxE (Ordinal iI)).
 Qed.
 
 Lemma fact_sqr_exp a p :
-   prime p -> 0 < a < p -> ~~ res_quad p a ->  (p.-1`!) = a ^ p.-1./2 %[mod p].
+   prime p -> ~~ (p %| a) -> ~~ res_quad p a ->  (p.-1`!) = a ^ p.-1./2 %[mod p].
 Proof.
-move=> pP aLp aR.
+move=> pP pNDa aR.
 have -> : p.-1`! = \prod_(i in 'F_p | i != 0%R) i.
   apply: etrans (_ : \prod_(i in 'F_p | i != 0 :> nat) i = _); last first.
     by apply: eq_bigl => i.
   rewrite /= Fp_cast //.
   rewrite fact_prod big_add1 /= big_mkord.
-  case: p {aLp aR}pP => //= p pP.
+  case: p {pNDa aR}pP => //= p pP.
   by rewrite [RHS]big_mkcond /= big_ord_recl /= mul1n.
 pose a' : 'F_p := inZp a.
+have a'E : a' = a %% p :> nat by rewrite /= Fp_cast.
 have a'_neq0 : a' != 0%R.
-  apply/eqP=> /val_eqP /=.
-  rewrite Fp_cast // modn_small; first by case: (a) aLp.
-  by case/andP: aLp.
+  apply/eqP/val_eqP; rewrite [val a']a'E /=.
+  by have /negPf := pNDa; rewrite /dvdn => ->.
+rewrite -modnXm -a'E.
 pose f (i : 'F_p) : 'F_p := (a' / i)%R.
 have f_eq0 : f 0%R = 0%R by rewrite /f GRing.invr0 GRing.mulr0.
 have fM (i : 'F_p) : i != ord0 -> (f i * i = a')%R.
@@ -65,7 +66,7 @@ have fI_neq0 (i : 'F_p) : i != 0%R -> f i != i.
   have /res_quadPn/(_ (Ordinal iL)) /= := aR.
   have /val_eqP := fM _ i_neq0; rewrite fiE /=.
   rewrite ![X in _ %% X]Fp_cast //= => /eqP->.
-  by rewrite modn_small ?eqxx // Fp_cast; case/andP: aLp.
+  by rewrite Fp_cast // eqxx.
 have fB : {on [pred i |  i != ord0],  bijective f}.
   by exists f => j _; apply: fI.
 pose can (i : 'F_p) :=  if i < (f i) then i else f i.
@@ -92,14 +93,11 @@ apply: etrans (_ : \prod_(j in 'F_p | j < f j) (j * f j) = _ %[mod p]).
   rewrite /can; case: leqP; last by case: (i =P j); rewrite andbF.
   case: (f i =P j); rewrite ?andbF // => <-.
   by rewrite fI eqxx andbF.
-apply: etrans (_ : \prod_(j in 'F_p | j < f j) a = _ %[mod p]).
+apply: etrans (_ : \prod_(j in 'F_p | j < f j) a' = _ %[mod p]).
   rewrite -modn_prodm; congr (_ %% _); apply: eq_bigr => i /andP[_ iLfi].
   have i_neq0 : i != 0%R.
     by apply/eqP=> i_eq0; rewrite i_eq0 f_eq0 ltnn in iLfi.
-  have /val_eqP/eqP := fM i i_neq0.
-  have -> : val a' = a.
-    by rewrite /= modn_small // Fp_cast; case/andP: aLp.
-  move=> <- //=; rewrite mulnC.
+  rewrite -(fM i i_neq0) mulnC.
   by congr (_ %% _); rewrite Fp_cast.
 congr (_ %% _).
 rewrite prod_nat_const.
@@ -130,25 +128,28 @@ by case: eqP => // ->; rewrite f_eq0 ltnn.
 Qed.
 
 Lemma euler_criterion a p : 
-  prime p -> 0 < a < p -> 
+  prime p -> ~~ (p %| a) -> 
   a ^ p.-1./2 = (if res_quad p a then 1 else p.-1) %[mod p].
 Proof.
-move=> pP aLp.
+move=> pP pNDa.
 have p_gt0 : 0 < p by apply: prime_gt0.
 have [/res_quadP[i Hi]|Hrn] := boolP (res_quad p a); last first.
   rewrite -fact_sqr_exp //.
   apply/eqP; rewrite -(eqn_modDr 1) !addn1 prednK //.
   have /dvdnP[k->] : (p %| (p.-1)`!.+1) by rewrite -Wilson // prime_gt1.
   by rewrite modnn modnMl.
-rewrite -modnXm -Hi modn_mod modnXm mulnn -expnM mul2n.
+rewrite -modnXm -Hi modnXm mulnn -expnM mul2n.
 have [pO|/(prime_oddPn pP) pE2]:= boolP (odd p); last first.
   by rewrite [in X in _ ^ X]pE2 /= expn0.
-have i_gt0 : 0 < i by case: i Hi aLp => [] [] //= _ <-; rewrite mod0n.
+have i_gt0 : 0 < i.
+  case: i Hi pNDa => [] [] //= _.
+  by rewrite /dvdn => <- /[!mod0n].
 rewrite even_halfK; last by case: (p) pP pO.
 apply/eqP; rewrite eqn_mod_dvd //; last by rewrite expn_gt0 i_gt0.
 rewrite -(Gauss_dvdr _ (_ : coprime _ i)); last first.
   rewrite prime_coprime //; apply/negP => /dvdnP [k iE].
-  by rewrite -Hi iE mulnA modnMl in aLp.
+  rewrite iE mulnA modnMl in Hi.
+  by case/negP: pNDa; rewrite /dvdn -Hi.
 rewrite mulnBr muln1 -expnS prednK //.
 rewrite -eqn_mod_dvd //; first by apply/eqP/fermat_little.
 by apply: leq_pexp2l (_ : 1 <= p).