proposition: Lemma mulrzBl_nat (m n : nat) x : x *~ (m%:Z - n%:Z) = x *~ m - x *~ n.
proof: Proof. case: (leqP m n)=> hmn; rewrite /intmul //=. rewrite addrC -{1}[m:int]opprK -opprD subzn //. rewrite -{2}[n](@subnKC m)// mulrnDr opprD addrA subrr sub0r. by case hdmn: (_ - _)%N=> [|dmn] /=; first by rewrite mulr0n oppr0. have hnm := ltnW hmn. rewrite -{2}[m](@subnKC n)// mulrnDr addrAC subrr add0r. by rewrite subzn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)