From mathcomp Require Import all_ssreflect all_algebra all_field.
Require Import gauss_int.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory Num.Theory UnityRootTheory.

Open Scope nat_scope.

Definition sum_of_two_square := 
  [qualify a x |
       [exists a : 'I_x.+1, exists b : 'I_x.+1, x == a ^ 2 + b ^ 2]].

Lemma sum2sP x :
  reflect (exists m, exists n, x = m ^ 2 + n ^ 2) 
          (x \is a sum_of_two_square).
Proof.
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: (iffP existsP) => [[m /existsP[n /eqP->]]|[m [n ->]]].
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by exists m; exists n.
have F1 : m <  (m ^ 2 + n ^ 2).+1.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
  rewrite ltnS (leq_trans _ (leq_addr _ _)) //.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by case: m => [|[|m]] //; rewrite (leq_exp2l 1).
have F2 : n <  (m ^ 2 + n ^ 2).+1.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
  rewrite ltnS (leq_trans _ (leq_addl _ _)) //.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by case: (n) => [|[|n1]] //; rewrite (leq_exp2l 1).
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by exists (Ordinal F1); apply/existsP; exists (Ordinal F2).
Qed.

Fact sum2s0 : 0 \is a sum_of_two_square.
Proof. by apply/sum2sP; exists 0; exists 0. Qed.

Fact sum2s1 : 1 \is a sum_of_two_square.
Proof. by apply/sum2sP; exists 0; exists 1. Qed.

Fact sum2s2 : 2 \is a sum_of_two_square.
Proof. by apply/sum2sP; exists 1; exists 1. Qed.

Fact sum2sX_even x n :
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
 ~~ odd n  -> x ^ n \is  a sum_of_two_square.
Proof.
(* Goal: forall _ : is_true (negb (odd n)), is_true (@in_mem nat (expn x n) (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
move=> En; apply/sum2sP; exists (x ^ n./2); exists 0.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by rewrite addn0 -{1}[n]odd_double_half (negPf En) -expnM muln2.
Qed.

Lemma sum2sGP x :
  reflect (exists m : GI, x = normGI m)
          (x \is a sum_of_two_square).
Proof.
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: (iffP idP) => [/sum2sP[m [n ->]]|[x1->]].
(* Goal: @ex GI (fun m0 : GI => @eq nat (addn (expn m (S (S O))) (expn n (S (S O)))) (normGI m0)) *)
(* Goal: is_true (@in_mem nat (normGI x1) (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
exists (m%:R + iGI * n%:R)%R.
  by rewrite normGIE /= !algGI_nat Re_rect ?Im_rect 
             ?CrealE ?conjC_nat ?natCK // !normr_nat !natCK.
(* Goal: is_true (@in_mem nat (normGI x1) (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite normGIE; set m := truncC _; set n := truncC _.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by apply/sum2sP; exists m; exists n.
Qed.

Lemma sum2sM x y :
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  x \is  a sum_of_two_square ->
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  y \is  a sum_of_two_square ->
  x * y \is  a sum_of_two_square.
Proof.
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))), is_true (@in_mem nat (expn x n) (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
move=> /sum2sGP[x1->] /sum2sGP[y1->]; rewrite -normGIM.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by apply/sum2sGP; exists (x1 * y1)%R.
Qed.

Lemma sum2s_dvd_prime p a b :
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  prime p -> coprime a b -> 
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  p %| a ^ 2 + b ^ 2 -> p \is  a sum_of_two_square.
Proof.
(* Goal: forall (_ : is_true (prime p)) (_ : is_true (coprime a b)) (_ : is_true (dvdn p (addn (expn a (S (S O))) (expn b (S (S O)))))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
move=> Pp Cab pDab.
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
have /dvdGI_norm := pdivGI_dvd (p%:R); set x := pdivGI _.
(* Goal: is_true (andb true (dvdn p b)) *)
have Px : primeGI x.
(* Goal: is_true (primeGI x) *)
(* Goal: forall _ : is_true (dvdn (normGI x) (normGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  apply: pdivGI_prime; rewrite normGI_nat.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by rewrite -{1}(expn0 p) ltn_exp2l // prime_gt1.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Re Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb (dvdn p a) (dvdn p b)) *)
rewrite (normGI_nat p)=> /(dvdn_pfactor _ _ Pp)=> [[[|[|[]]]]] _ //.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
- by move=> H; case/andP: Px; rewrite H ltnn.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
- by rewrite expn1=> H; apply/sum2sGP; exists x.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -normGI_nat => H1.
(* Goal: is_true (andb true (dvdn p b)) *)
have PGIp : primeGI (p%:R).
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
 apply: eqGI_prime Px.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
 by apply: dvdGI_eq_norm (pdivGI_dvd _).
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
pose z := (a%:R + iGI * b%:R)%R.
(* Goal: is_true (andb true (dvdn p b)) *)
have F : ('N z)%GI = a ^ 2 + b ^ 2.
  by rewrite normGIE /= !algGI_nat !(Re_rect, Im_rect)
            ?Creal_Cnat // !normr_nat !natCK.
(* Goal: is_true (andb true (dvdn p b)) *)
have F1 : (p%:R %| z * conjGI z)%GI%R.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
  rewrite conjGIM_norm F.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  case/dvdnP: pDab => q1 ->.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by apply/dvdGIP; exists (q1%:R); rewrite natrM.
(* Goal: is_true (andb true (dvdn p b)) *)
have []: ~ (p %| gcdn a b).
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by rewrite (eqP Cab) Euclid_dvd1.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
rewrite dvdn_gcd.
(* Goal: is_true (andb true (dvdn p b)) *)
have [F2|] := boolP (p%:R %| z)%GI.
(* Goal: is_true (andb true (dvdn p b)) *)
  have := dvdGI_nat_dvdz_Re F2.
  rewrite Re_rect /= algGI_nat ?Creal_Cnat //=
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
           (intCK (Posz a)) /= => ->.
(* Goal: is_true (andb true (dvdn p b)) *)
  have := dvdGI_nat_dvdz_Im F2.
  by rewrite Im_rect /= algGI_nat ?Creal_Cnat //=
           (intCK (Posz b)).
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -primeGI_coprime // => HH.
(* Goal: is_true (andb true (dvdn p b)) *)
have F2 : (p%:R %| conjGI z)%GI.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  by rewrite -(Gauss_dvdGIr _ HH).
(* Goal: is_true (andb true (dvdn p b)) *)
have := dvdGI_nat_dvdz_Re F2.
rewrite Re_conj Re_rect /= algGI_nat ?Creal_Cnat //=
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
           (intCK (Posz a)) => ->.
(* Goal: is_true (andb true (dvdn p b)) *)
have := dvdGI_nat_dvdz_Im F2.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
rewrite Im_conj Im_rect /= algGI_nat ?Creal_Cnat //=.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by rewrite floorCN ?Cint_Cnat // abszN (intCK (Posz b)).
Qed.

Lemma sum2sX x n :
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  x \is  a sum_of_two_square  -> x ^ n \is  a sum_of_two_square.
Proof.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
move=>/sum2sGP[x1->]; rewrite -normGIX.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by apply/sum2sGP; exists (x1 ^+ n)%R.
Qed.

Lemma sum2sX_prime x n :
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  prime x -> odd n ->
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  x ^ n \is  a sum_of_two_square -> x  \is  a sum_of_two_square.
Proof.
(* Goal: forall (_ : is_true (prime p)) (_ : is_true (coprime a b)) (_ : is_true (dvdn p (addn (expn a (S (S O))) (expn b (S (S O)))))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
move=> Px On /sum2sP[a [b adE]].
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
pose u := gcdn a b.
(* Goal: is_true (andb true (dvdn p b)) *)
have /(dvdn_pfactor _ _ Px)[m] : u ^ 2 %| x ^ n.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by rewrite adE dvdn_add // dvdn_exp2r ?(dvdn_gcdr, dvdn_gcdl).
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite leq_eqVlt => /orP[/eqP->|nLM] uE.
  move: On; have := congr1 (logn x) uE.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  rewrite (pfactorK _ Px) lognX => <-.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by rewrite mul2n odd_double.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
have /(sum2s_dvd_prime _ _)->//: x %| (a %/ u) ^ 2 + (b %/ u) ^ 2.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  apply/dvdnP; exists (x^(n-m).-1); apply/eqP.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
    rewrite -expnSr prednK ?subn_gt0 //.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
    have/eqn_pmul2r<- : (0 < x ^ m) by rewrite expn_gt0 prime_gt0.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
    by rewrite -{1}uE mulnDl -!expnMn -expnD subnK 1?ltnW //
            !divnK ?(adE, dvdn_gcdr, dvdn_gcdl).
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
rewrite /coprime.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
have/eqn_pmul2r<- : (0 < u).
(* Goal: is_true (andb true (dvdn p b)) *)
  have: (0 < u ^ 2) by rewrite uE expn_gt0 prime_gt0.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by case: (u).
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by rewrite muln_gcdl mul1n !divnK ?(adE, dvdn_gcdr, dvdn_gcdl).
Qed.

Lemma sum2sM_coprime x y :
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  coprime x y ->
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  x * y \is  a sum_of_two_square ->  x \is  a sum_of_two_square.
Proof.
(* Goal: forall (_ : is_true (prime p)) (_ : is_true (coprime a b)) (_ : is_true (dvdn p (addn (expn a (S (S O))) (expn b (S (S O)))))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
move=> Cxy /sum2sGP[z Hz].
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
pose t := gcdGI (x%:R) z.
apply/sum2sGP; exists t.
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: eqGI_nat.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -conjGIM_norm.
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: eqGI_trans (_ : eqGI (t * gcdGI (x%:R) (conjGI z))%R _).
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  apply: gcdGI_mull_equiv (coprimeGI_nat Cxy) _.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  by rewrite -natrM Hz conjGIM_norm.
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: eqGI_mul (eqGIxx _) _.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
by rewrite -conjGI_nat eqGI_sym conjGI_gcd.
Qed.

Lemma modn_prod I r (P : pred I) F d :
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  \prod_(i <- r | P i) (F i %% d) = \prod_(i <- r | P i) F i %[mod d].
Proof.
(* Goal: @eq nat (modn (@BigOp.bigop nat I (S O) r (fun i : I => @BigBody nat I i muln (P i) (modn (F i) d))) d) (modn (@BigOp.bigop nat I (S O) r (fun i : I => @BigBody nat I i muln (P i) (F i))) d) *)
apply/eqP; elim/big_rec2: _ => // i m n _.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
by rewrite modnMml -modnMmr => /eqP->; rewrite modnMmr.
Qed.

Lemma sum2sprime p : 
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  odd p -> prime p -> p \is a sum_of_two_square = (p %% 4 == 1).
Proof.
move=> Op Pp; apply/idP/idP=>[/sum2sP[a [b H]]|pM4].
(* Goal: is_true (andb true (dvdn p b)) *)
  have F c : (c ^ 2 %% 4 == 0) || (c ^ 2 %% 4 == 1).
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
    rewrite -modnXm expnS expn1.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
    by move: (c %% 4) (ltn_pmod c (isT: 0 < 4)); do 4 case => //.
(* Goal: is_true (andb true (dvdn p b)) *)
  have : (p %% 4 == 1) || (p %% 4 == 3).
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
    rewrite -[p]odd_double_half Op -modnDmr -muln2.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
    have /(_ _ 2)<- := muln_modl (isT: 0 < 2).
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
    by move: (_ %% 2) (ltn_pmod p./2 (isT: 0 < 2)); do 2 case => //.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  rewrite H -modnDm.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  by move: (F a) (F b) => /orP[] /eqP-> /orP[] /eqP->.
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
pose k := p %/ 4.
(* Goal: is_true (andb true (dvdn p b)) *)
have p_gt0 := prime_gt0 Pp.
(* Goal: is_true (andb true (dvdn p b)) *)
have p_gt1 := prime_gt1 Pp.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
have : (p.-1)`!.+1 %% p == 0 by rewrite -[_ == 0]Wilson.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
have : \prod_(1 <= i < (k * 2).+1) (p - 1) = 1 %[mod p].
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
  rewrite prod_nat_const_nat !subn1 /= mulnC expnM.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  rewrite -modnXm expnS expn1.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  rewrite -[_ * _ %% _]modnDr -{3}[p]prednK -addn1 //.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  by rewrite addnA -mulnSr prednK // modnMDl modnXm exp1n.
(* Goal: is_true (andb true (dvdn p b)) *)
have pE : p = (k * 4).+1 by rewrite (divn_eq p 4) (eqP pM4) addn1.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Re Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb (dvdn p a) (dvdn p b)) *)
rewrite pE => F.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
have [/eqP-> _|] := boolP (k == 0); first exact: sum2s1.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -leqn0 -ltnNge => Pk.
rewrite fact_prod (big_cat_nat _ _ _ (_ : 1 <= (k * 2).+1)) //=; last first.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by rewrite ltnS leq_mul2l orbT.
set S1 := \prod_(_ <= _ < _ ) _.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -addn1 -modnDml -modnMmr big_nat_rev /=.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -[(k * 2).+1]add1n big_addn.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite subSn ?leq_pmul2l // -mulnBr /=.
set S2 := \prod_(_ <= _ < _ ) _.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -[S2]muln1 -[S2 * 1 %% _]modnMmr -{}F.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
rewrite [S2 * _ %% _]modnMmr.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -[S2 * _]big_split /=.
set S3 := \prod_(_ <= _ < _ ) _.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
suff ->: S3 = S1 %[mod (k * 4).+1].
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  rewrite modnMmr modnDml -{1}[S1]expn1 -expnSr -[S1]fact_prod.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  rewrite -pE -{3}[1](exp1n 2) => /sum2s_dvd_prime-> //.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by rewrite coprimen1.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -modn_prod -[in RHS]modn_prod.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
rewrite big_nat_cond [in RHS]big_nat_cond.
congr (_ %% _).
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: eq_bigr => i /andP[/andP[H1 H2] _].
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite add1n addnC -addnS [i + _]addnC subnDA addnK.
(* Goal: is_true (andb true (dvdn p b)) *)
have H3 : i <= (k * 4).+1.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
  by rewrite ltnW // (leq_trans H2) // ltnS leq_pmul2l.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -modnDr -{3}(subnK H3) addnA -mulnSr subn1 prednK //.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by rewrite modnMDl.
Qed.

(** Main theorem **)
Lemma sum2stest n :
  reflect
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  (forall p,  prime p -> odd p -> p %| n -> odd (logn p n) -> p %% 4 = 1)
  (n \is a sum_of_two_square).
Proof.
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: (iffP idP) => [Hs p Pp Op Dp OL|HH].
(* Goal: is_true (andb true (dvdn p b)) *)
  have Pn : 0 < n by case: (n) OL; rewrite ?logn0.
(* Goal: is_true (andb true (dvdn p b)) *)
  have /(pfactor_coprime Pp)[m Cmp mE] := (Pn).
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  apply/eqP; rewrite -sum2sprime //.
  apply:  sum2sX_prime OL _ => //.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
  rewrite mE mulnC in Hs.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
  by apply: sum2sM_coprime Hs; rewrite coprime_pexpl // -pfactor_dvdn.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
have [/eqP->|] := boolP (n == 0); first by apply:sum2s0.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite -leqn0 -ltnNge => /prod_prime_decomp->.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Im Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb true (dvdn p b)) *)
rewrite big_seq_cond /=.
elim/big_rec: _ => [|i x /andP[]].
exact: sum2s1.
(* Goal: forall _ : is_true (dvdn p (absz (floorC (@Re Algebraics.Implementation.numClosedFieldType (algGI (conjGI z)))))), is_true (andb (dvdn p a) (dvdn p b)) *)
rewrite prime_decompE => /mapP[p].
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
rewrite mem_primes => /and3P[Pp Pn pDn] -> _ xS /=.
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: sum2sM => //.
have [OL|] := boolP (odd (logn p n)); last by exact: sum2sX_even.
(* Goal: is_true (primeGI (@GRing.natmul (GRing.Ring.zmodType GI_ringType) (GRing.one GI_ringType) p)) *)
(* Goal: is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
apply: sum2sX.
(* Goal: forall _ : @eq nat (normGI x) (expn p (S O)), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
(* Goal: forall _ : @eq nat (normGI x) (expn p (S (S O))), is_true (@in_mem nat p (@mem nat (predPredType nat) (@has_quality (S O) nat sum_of_two_square))) *)
have [Op|/prime_oddPn->//] := boolP (odd p); last by exact: sum2s2.
(* Goal: forall _ : is_true (@eq_op nat_eqType (modn n d) (modn m d)), is_true (@eq_op nat_eqType (modn (muln (modn (F i) d) n) d) (modn (muln (F i) m) d)) *)
by rewrite sum2sprime // HH.
Qed.
