proposition: Lemma abse_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) (x : {compare (0 : \bar R) & xnz & xr}) (r := abse_reality_subdef xnz xr) : Signed.spec 0 xnz r `|x%:num|.
proof: Proof. rewrite {}/r; case: xr xnz x => [[[]|]|] [] x //=; do ?[by case: (bottom x)|by rewrite eq0 abse0 |by rewrite abse_ge0// andbT gee0_abs |by rewrite abse_ge0// andbT lee0_abs |by rewrite abse_ge0// andbT abse_eq0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed