proposition: Lemma sn2bin n: \sum_(i<n.+1) i ^2 = T_nkbin n 1.
proof: Proof. by rewrite F6aux /T_nkbin mul2n - addnn addnCA (addnC 'C(n.+1, 2)) - binS addn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)