proposition: Lemma F7a n: 'C(n, 2) + 6 * 'C(n.+1, 4) = 'C(n, 2) ^ 2.
proof: Proof. case:n => // n; apply /eqP; rewrite - (eqn_pmul2l (ltn0Sn 3)); apply /eqP. rewrite mulnDr - (expnMn 2 _ 2) - (mulnA 2 2) mulnCA - (mulnA 2 3). rewrite - 2!mul_bin_diag bin1 (mulnCA 3) - !mul_bin_diag mulnCA. rewrite (mulnCA 2) (mulnCA 2) (mulnCA n.+2) - mulnDr; case:n => //n. rewrite - !mul_bin_diag bin1 (mulnC _ n) mulnA - mulnDl - mulnn - mulnA. by rewrite (mulnC n.+1) - {2} (add2n n) (mulSn _ n) addnA add2n - mulnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)