proposition: Fact Op_N_natmul_subproof (n : N) (m : nat) : Z.of_N (n *+ m)%R = (Z.of_N n * Z.of_nat m)%Z.
proof: Proof. by rewrite raddfMn -mulr_natr -[m in RHS]natn rmorph_nat. Qed.
imports: Coq(ZArith ZifyClasses ZifyBool) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial ssralg countalg ssrnum ssrint rat) mathcomp(intdiv) mathcomp(zify_ssreflect ssrZ)