proposition: Lemma sqrtc_sqrtr : forall (x : R[i]), 0 <= x -> sqrtc x = (sqrtr (Re x))%:C.
proof: Proof. move=> [a b] /andP [/eqP->] /= a_ge0. rewrite eqxx mul1r [0 ^+ _]exprS mul0r addr0 sqrtr_sqr. rewrite ger0_norm // subrr mul0r sqrtr0 -mulr2n. by rewrite -[_*+2]mulr_natr mulfK // pnatr_eq0. 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)