proposition: Lemma exprM x m n : x ^+ (m * n) = x ^+ m ^+ n.
proof: Proof. elim: m => [|m IHm]; first by rewrite expr1n. by rewrite mulSn exprD IHm exprS exprMn_comm //; apply: commrX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)