proposition: Lemma intmul_snum_subproof (xnz nnz : nullity) (xr nr : reality) (x : {num R & xnz & xr}) (n : {num int & nnz & nr}) (rnz := mul_nonzero_subdef xnz nnz xr nr) (rrl := mul_reality_subdef xnz nnz xr nr) : Signed.spec 0 rnz rrl (x%:num *~ n%:num).
proof: Proof. rewrite {}/rnz {}/rrl; apply/andP; split. by move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n; rewrite mulrz_neq0//= ?neq0. move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x n //; do ?[by case: (bottom x)|by case: (bottom n) |by rewrite mulrz_ge0|by rewrite mulrz_le0_ge0|by rewrite eq0 mul0rz |by rewrite mulrz_ge0_le0|by rewrite mulrz_le0|by rewrite eq0 mulr0z |by rewrite -realE rpredMz//; apply: cmp0]. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)