proposition: Lemma Cat_dvd n k: k <= n -> Cat' n k = n.+1 * Cat n k.
proof: Proof. elim: n k; first by move => k; rewrite leqn0 => /eqP ->. move => n H; elim; first by rewrite /Cat /Cat' {1}mulnC addn0 subn0 mulnK //. move => k HH; rewrite ltnS; rewrite leq_eqVlt => /orP; case => np. by rewrite (eqP np) /Cat /Cat' subSS addnn subSnn muln1 catalan_prop. move /eqP: (Cat_rec_aux (ltnW np)); rewrite /Cat -/(Cat' _ _) (H _ np) mulnCA. rewrite - mulnDr eqn_pmul2l // (HH (ltnW (ltn_trans np (ltnSn n)))) - mulnDr. by move /eqP ->;rewrite mulKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)