proposition: Lemma catalan_rec n: (n.+2) * catalan n.+1 = (n.*2.+1.*2) * catalan n.
proof: Proof. apply/eqP. have ha m: 0 < ((m`!)^2 * m.+1) by rewrite muln_gt0 expn_gt0 fact_gt0 //. rewrite -(eqn_pmul2l (ha n.+1)) mulnCA catalan_fact mulnA -(eqn_pmul2l (ha n)). rewrite [in X in _== X] mulnCA catalan_fact doubleS factS - doubleS. rewrite - muln2 - (mulnA _ 2) mulnCA (mulnC _ n.+2) -2! (mulnA n.+2). rewrite -(mulnA _ _ (n.*2)`!) - (mul2n (n.*2.+1)) - (mulnA 2) - factS -mulnA. by rewrite (mulnA n.+1) mulnn (mulnA (n`! ^ 2)) -expnMn -factSr eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)