proposition: Lemma F6_aux n: n ^2 = 2 * 'C(n,2) + 'C(n,1).
proof: Proof. case: n => // n; rewrite bin2 bin1 succnK mul2n - mulnn mulnSr. by move:(odd_double_half (n.+1 * n)); rewrite oddM /= andNb add0n => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)