proposition: Lemma opp_snum_subproof (xnz : nullity) (xr : reality) (x : {num R & xnz & xr}) (r := opp_reality_subdef xnz xr) : Signed.spec 0 xnz r (- x%:num).
proof: Proof. by rewrite {}/r; case: xr x => [[[]|]|]//= [r]/=; rewrite oppr_eq0 ?(oppr_ge0, oppr_le0)// orbC. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)