proposition: Fact mulrzDl_tmp m : {morph ( *~%R^~ m : M -> M) : x y / x + y}.
proof: Proof. by elim: m=> [|m _|m _] x y; rewrite ?addr0 /intmul //= ?mulrnDl // opprD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)