proposition: Lemma Cat_rec_aux n k: k <= n -> n.+1 * Cat' n.+1 k.+1 = n.+2 * Cat' n k.+1 + n.+1* Cat' n.+1 k.
proof: Proof. move => h; apply /eqP; rewrite /Cat'. rewrite mulnCA (mulnCA n.+2) (mulnCA n.+1). have pp: 0 < n`! * (k.+1)`! by rewrite muln_gt0 !fact_gt0 . rewrite -(eqn_pmul2r pp) mulnDl -mulnA mulnACA -factS( mulnCA (n.+1)`!) mulnCA. rewrite - {3} (addKn n.+1 k.+1) (bin_fact (leq_addr k.+1 n.+1)) mulnAC. rewrite - {4} (addKn n k.+1) (bin_fact (leq_addr k.+1 n)) - mulnA mulnACA. rewrite - factS (factSr k) (mulnCA _ k`!) (mulnA (n.+1)`!) 2! mulnA mulnA. rewrite -{6}(addKn n.+1 k) (bin_fact (leq_addr k n.+1)) -2!mulnA -(addSnnS n). rewrite - mulnDr mulnC addnS factSr - mulnA 2!subSS;apply/eqP; congr muln. rewrite (subSn (leq_trans h (leqnSn n))) (subSn h) -addSn mulnSr mulnSr. rewrite addnA 2!(mulSnr _ k) (mulnC _ k) (addnAC _ k) -(addnA _ k) 2!(addnS k). by rewrite (subnKC h) -2!(addnA _ _ k) [RHS] addnA - mulnDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)