proposition: Lemma F13' n: \sum_(i<n) (i.*2.+1)^2 = 8 * 'C(n.+1,3) + 'C(n,1).
proof: Proof. elim :n => //; first by rewrite big_ord0 bin0n. move => n Hrec; rewrite big_ord_recr Hrec /= (binS (n.+1)) mulnDr !bin1. rewrite addnAC -{4} (add1n n) addnA - (addnA _ _ 1); congr (_ + _ + _). rewrite -(mulnA 4 2) -mul_bin_diag bin1 -addn1 sqrnD - !mulnn !muln1 addnAC. by rewrite - mulnDl mulnA (mulnAC 2 2) - mulnA (mul2n n) mulnSr mul2n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)