proposition: Lemma mul_snum_subproof (xnz ynz : nullity) (xr yr : reality) (x : {num R & xnz & xr}) (y : {num R & ynz & yr}) (rnz := mul_nonzero_subdef xnz ynz xr yr) (rrl := mul_reality_subdef xnz ynz xr yr) : Signed.spec 0 rnz rrl (x%:num * y%:num).
proof: Proof. rewrite {}/rnz {}/rrl; apply/andP; split. by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []// x y; rewrite mulf_neq0. by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //; do ?[by rewrite mulr_ge0|by rewrite mulr_le0_ge0 |by rewrite mulr_ge0_le0|by rewrite mulr_le0|by rewrite -realE realM |by case: (bottom x)|by case: (bottom y)|by rewrite eq0 ?mulr0// mul0r]. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)