proposition: Lemma bin_fact2n_g i: 0 < i -> (i.+2) * 'C(i.*2, i) + (3*i.+1) * 'C(i.*2, i.-1) = (i.+1) * 'C((i.+1).*2, i.+1).
proof: Proof. move => h; apply/eqP. have ha: 0 < (i.+1)`!^2 by rewrite expn_gt0 fact_gt0. rewrite - (eqn_pmul2r ha) -(mulnA i.+1) (bin_fact2n_a i.+1) mulnDl factS. rewrite {1} expnMn -mulnA. rewrite (mulnC (i.+1 ^ 2)) (mulnA _ _ (i.+1 ^ 2)) bin_fact2n_a -(mulnn (_ * _)). rewrite - {2} factS -(mulnA (i.+1)) mulnACA (bin_fact2n_b h) -(mulnA 3) mulnn. rewrite (mulnC _ i) mulnACA (mulnC (_ ^ 2)) - mulnDl 2!addSn -mulSn. rewrite -(mulnA 2 2) 2!mul2n - doubleS - muln2 - mulnA (mulnCA 2) mulnA -factS. by rewrite - mulnn (mulnA 2) mul2n doubleS mulnA -factSr mulnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)