proposition: Lemma exprD1n x n : (x + 1) ^+ n = \sum_(i < n.+1) x ^+ i *+ 'C(n, i).
proof: Proof. rewrite addrC (exprDn_comm n (commr_sym (commr1 x))). by apply: eq_bigr => i _; rewrite expr1n mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)