proposition: Lemma sqrt_snum_subproof xnz xr (x : {num R & xnz & xr}) (nz := sqrt_nonzero_subdef xnz xr) : Signed.spec 0 nz >=0 (Num.sqrt x%:num).
proof: Proof. by rewrite {}/nz; case: xnz xr x => -[[[]|]|]//= x; rewrite /= sqrtr_ge0// andbT sqrtr_eq0 le0F. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)