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