proposition: Lemma sqr_sqrtc : forall x, (sqrtc x) ^+ 2 = x.
proof: Proof. have sqr: forall x : R, x ^+ 2 = x * x. by move=> x; rewrite exprS expr1. case=> a b; rewrite exprS expr1; simpc. have F0: 2%:R != 0 :> R by rewrite pnatr_eq0. have F1: 0 <= 2%:R^-1 :> R by rewrite invr_ge0 ler0n. have F2: `|a| <= sqrtr (a^+2 + b^+2). rewrite -sqrtr_sqr ler_wsqrtr //. by rewrite addrC -subr_ge0 addrK exprn_even_ge0. have F3: 0 <= (sqrtr (a ^+ 2 + b ^+ 2) - a) / 2%:R. rewrite mulr_ge0 // subr_ge0 (le_trans _ F2) //. by rewrite -(maxrN a) le_maxr lexx. have F4: 0 <= (sqrtr (a ^+ 2 + b ^+ 2) + a) / 2%:R. rewrite mulr_ge0 // -{2}[a]opprK subr_ge0 (le_trans _ F2) //. by rewrite -(maxrN a) le_maxr lexx orbT. congr (_ +i* _); set u := if _ then _ else _. rewrite mulrCA !mulrA. have->: (u * u) = 1. rewrite /u; case: (altP (_ =P _)); rewrite ?mul1r //. by rewrite -expr2 sqr_sg => ->. rewrite mul1r -!sqr !sqr_sqrtr //. rewrite [_+a]addrC -mulrBl opprD addrA addrK. by rewrite opprK -mulr2n -[a *+ 2]mulr_natl [_*a]mulrC mulfK. rewrite mulrCA -mulrA -mulrDr [sqrtr _ * _]mulrC. rewrite -mulr2n -sqrtrM // mulrAC !mulrA ?[_ * (_ - _)]mulrC -subr_sqr. rewrite sqr_sqrtr; last first. by rewrite ler_paddr // exprn_even_ge0. rewrite [_^+2 + _]addrC addrK -mulrA -expr2 sqrtrM ?exprn_even_ge0 //. rewrite !sqrtr_sqr -(mulr_natr (_ * _)). rewrite [`|_^-1|]ger0_norm // -mulrA [_ * _%:R]mulrC divff //. rewrite mulr1 /u; case: (_ =P _)=>[->|]. by rewrite normr0 mulr0. by rewrite mulr_sg_norm. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)