proposition: Theorem Pascal a b n : (a + b) ^ n = \sum_(i < n.+1) 'C(n, i) * (a ^ (n - i) * b ^ i).
proof: Proof. elim: n => [|n IHn]; rewrite big_ord_recl muln1 ?big_ord0 //. rewrite expnS {}IHn /= mulnDl !big_distrr /= big_ord_recl muln1 subn0. rewrite !big_ord_recr /= !binn !subnn bin0 !subn0 !mul1n -!expnS -addnA. congr (_ + _); rewrite addnA -big_split /=; congr (_ + _). apply: eq_bigr => i _; rewrite mulnCA (mulnA a) -expnS subnSK //=. by rewrite (mulnC b) -2!mulnA -expnSr -mulnDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)