proposition: Lemma sqrtC_snum_subproof xnz xr (x : {num R & xnz & xr}) (r := sqrtC_reality_subdef xnz xr) : Signed.spec 0 xnz r (sqrtC x%:num).
proof: Proof. rewrite {}/r; apply/andP; split. by rewrite sqrtC_eq0; case: xr xnz x => [[[]|]|] [] /=. by case: xr xnz x => [[[]|]|] []//= x; rewrite ?sqrtC_ge0// sqrtC_eq0 eq0. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)