proposition: Lemma catalan_pos n: 0 < n -> catalan n = 'C(n.*2, n) - 'C(n.*2, n.-1).
proof: Proof. by rewrite /catalan;move => /bin_fact2n_e {1} <-;rewrite mulnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)