fact: Definition sqrt_nonzero_subdef (xnz : nullity) (xr : reality) := if xr is Real (Sign >=0) then xnz else MaybeZero.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)