proposition: Lemma F12 n: \sum_(i<n) (i.*2.+1) = n ^2.
proof: Proof. elim: n; first by rewrite big_ord0. move => n Hrec;rewrite big_ord_recr /= Hrec. rewrite - (addn1 n) sqrnD -addnA; congr (_ + _). by rewrite muln1 mulnC add1n muln2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)