proposition: Lemma add_snum_subproof (xnz ynz : nullity) (xr yr : reality) (x : {num R & xnz & xr}) (y : {num R & ynz & yr}) (rnz := add_nonzero_subdef xnz ynz xr yr) (rrl := add_reality_subdef xnz ynz xr yr) : Signed.spec 0 rnz rrl (x%:num + y%:num).
proof: Proof. rewrite {}/rnz {}/rrl; apply/andP; split. move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; by rewrite 1?addr_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT). have addr_le0 (a b : R) : a <= 0 -> b <= 0 -> a + b <= 0. by rewrite -!oppr_ge0 opprD; apply: addr_ge0. move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; do ?[by rewrite addr_ge0|by rewrite addr_le0|by rewrite -realE realD |by case: (bottom x)|by case: (bottom y)|by rewrite !eq0 addr0]. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)