fact: Definition exprn_reality_subdef (xnz nnz : nullity) (xr nr : reality) : reality := match xr, nr with | _, Real (Sign =0) => >=0 | Real (Sign =0), _ => (if nnz then =0 else >=0)%snum_sign | Real (Sign >=0), _ => >=0 | Real _, _ => >=<0 | _, _ => >?<0 end.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)