proposition: Lemma exprDn_comm x y n (cxy : comm x y) : (x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) * y ^+ i) *+ 'C(n, i).
proof: Proof. elim: n => [|n IHn]; rewrite big_ord_recl mulr1 ?big_ord0 ?addr0 //=. rewrite exprS {}IHn /= mulrDl !big_distrr /= big_ord_recl mulr1 subn0. rewrite !big_ord_recr /= !binn !subnn !mul1r !subn0 bin0 !exprS -addrA. congr (_ + _); rewrite addrA -big_split /=; congr (_ + _). apply: eq_bigr => i _; rewrite !mulrnAr !mulrA -exprS -subSn ?(valP i) //. by rewrite subSS (commrX _ (commr_sym cxy)) -mulrA -exprS -mulrnDr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)