proposition: Lemma sqrtc_ge0 (x : R[i]) : (0 <= sqrtc x) = (0 <= x).
proof: Proof. apply/idP/idP=> [psx|px]; last first. by rewrite sqrtc_sqrtr // lecR sqrtr_ge0. by rewrite -[x]sqr_sqrtc exprS expr1 mulr_ge0. 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)