fact: Definition abse_reality_subdef (xnz : KnownSign.nullity) (xr : KnownSign.reality) := (if xr is =0 then =0 else >=0)%snum_sign.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed