proposition: Lemma F6aux n: \sum_(i<n) i ^2 = 'C(n,2) + 2 * 'C(n,3).
proof: Proof. by rewrite sum_pow 3! big_ord_recr /= big_ord0 mul0n mul1n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)