proposition: Lemma oppe_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) (x : {compare (0 : \bar R) & xnz & xr}) (r := opp_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 ?eqe_oppLR ?oppe0 1?eq0//; rewrite ?oppe_le0 ?oppe_ge0 ?(eq0, eq0F, ge0, le0)//; rewrite orbC [_ || _]cmp0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed