proposition: Lemma dadde_snum_subproof (xnz ynz : KnownSign.nullity) (xr yr : KnownSign.reality) (x : {compare (0 : \bar R) & xnz & xr}) (y : {compare (0 : \bar R) & ynz & yr}) (rnz := add_nonzero_subdef xnz ynz xr yr) (rrl := add_reality_subdef xnz ynz xr yr) : Signed.spec 0 rnz rrl (dual_adde x%:num y%:num)%dE.
proof: Proof. rewrite {}/rnz {}/rrl; apply/andP; split. move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; by rewrite 1?dadde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT). move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; do ?[by case: (bottom x)|by case: (bottom y) |by rewrite dadde_ge0|by rewrite dadde_le0 |exact: realDed|by rewrite 2!eq0 /dual_adde/= addr0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed