proposition: Lemma catalan_prop n: n.+1 * catalan n = 'C(n.*2, n).
proof: Proof. move:(leq0n n); rewrite leq_eqVlt => /orP; case => np. by move/eqP:np => <-. by rewrite -(bin_fact2n_e np) mulnC (catalan_pos np). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)