proposition: Lemma iJ : conj i = - i.
proof: Proof. have nz2 := nz2. have /sqrtE[b]: conj i ^+ 2 = - 1 by rewrite -rmorphXn /= sqrtK rmorphN1. rewrite mulr_sign -/i; case: b => // Ri. case: conj_nt => z; wlog zJ: z / conj z = - z. move/(_ (z - conj z)); rewrite !rmorphB conjK opprB => zJ. by apply/mul2I/(canRL (subrK _)); rewrite -addrA zJ // addrC subrK. have [-> | nz_z] := eqVneq z 0; first exact: rmorph0. have [u Ru [v Rv Dz]]: exists2 u, conj u = u & exists2 v, conj v = v & (u + z * v) ^+ 2 = z. - pose y := sqrt z; exists ((y + conj y) / 2). by rewrite fmorph_div rmorphD /= conjK addrC rmorph_nat. exists ((y - conj y) / (z *+ 2)). rewrite fmorph_div rmorphMn /= zJ mulNrn invrN mulrN -mulNr rmorphB opprB. by rewrite conjK. rewrite -(mulr_natl z) invfM (mulrC z) !mulrA divfK // -mulrDl addrACA. by rewrite subrr addr0 -mulr2n -[_ *+ 2]mulr_natr mulfK ?Neq0 ?sqrtK. suff u0: u = 0 by rewrite -Dz u0 add0r rmorphXn rmorphM /= Rv zJ mulNr sqrrN. suff [b Du]: exists b : bool, u = (-1) ^+ b * i * z * v. apply: mul2I; rewrite mul0rn mulr2n -{2}Ru. by rewrite Du !rmorphM /= rmorph_sign Rv Ri zJ !mulrN mulNr subrr. have/eqP:= zJ; rewrite -addr_eq0 -{1 2}Dz rmorphXn rmorphD rmorphM /= Ru Rv zJ. rewrite mulNr sqrrB sqrrD addrACA (addrACA (u ^+ 2)) addNr addr0 -!mulr2n. rewrite -mulrnDl -(mul0rn _ 2) (inj_eq mul2I) /= -[rhs in _ + rhs]opprK. rewrite -sqrMi subr_eq0 eqf_sqr -mulNr !mulrA. by case/pred2P=> ->; [exists false | exists true]; rewrite mulr_sign. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)