proposition: Lemma Cat_rec n k: k <= n -> Cat n.+1 k.+1 = Cat n k.+1 + Cat n.+1 k.
proof: Proof. move => h; apply/eqP. have h':= (leq_ltn_trans h (ltnSn n)). have ww: Cat' n k.+1 = n.+1 * Cat n k.+1. move:h; rewrite leq_eqVlt => /orP; case => np; last by rewrite Cat_dvd. by rewrite /Cat /Cat' (eqP np) subnn muln0 div0n muln0. move /eqP:(Cat_rec_aux h); rewrite (Cat_dvd h') (Cat_dvd(ltnW h')) ww. by rewrite mulnCA (mulnCA n.+1) -mulnDr - mulnDr 2!mulnA eqn_pmul2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)