proposition: Lemma mule_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 := 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 mule_neq0. by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //; do ?[by case: (bottom x)|by case: (bottom y) |by rewrite mule_ge0|by rewrite mule_le0_ge0 |by rewrite mule_ge0_le0|by rewrite mule_le0|exact: realMe |by rewrite eq0 ?mule0// mul0e]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed