proposition: Fact mulrzDr_tmp x : {morph *~%R x : m n / m + n}.
proof: Proof. elim=> [|m _|m _]; elim=> [|n _|n _]; rewrite /intmul //=; rewrite -?(opprD) ?(add0r, addr0, mulrnDr, subn0) //. * by rewrite -/(intmul _ _) mulrzBl_nat. * by rewrite -/(intmul _ _) addrC mulrzBl_nat addrC. * by rewrite -addnS -addSn mulrnDr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)