proposition: Lemma catalan_prod n: (n.+1)`! * catalan n = \prod_(i<n) i.*2.+1.*2.
proof: Proof. elim:n => [| n Hr]; first by rewrite big_ord0. by rewrite factSr -mulnA catalan_rec mulnCA Hr mulnC big_ord_recr /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)