proposition: Lemma catalan_fact n: ((n`!)^2 * n.+1) * catalan n = (n.*2)`!.
proof: Proof. by rewrite -mulnA catalan_prop mulnC bin_fact2n_a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)