proposition: Lemma catalan_sum n: catalan n.+1 = \sum_(i<n.+1) catalan i * catalan (n-i).
proof: Proof. elim:n; first by rewrite big_ord_recr /= big_ord0. move => n Hr. Abort. Definition Tnk1 n k := 'C(n.*2.-1, n-k) - 'C(n.*2.-1, (n-k).-2). Definition Tnk2 n k := ('C(n.*2, n-k) * (k.*2.+1)) %/ (n+k+1). Lemma Tnk2_alt n k: k.+1 <= n -> (k.*2.+1)* 'C(n.*2, n-k) = (n+k).+1 * ('C(n.*2, (n-k)) - 'C(n.*2, n-k-1)). Proof. move => h; apply/eqP. have ha: n + k + (n - k) = n.*2 by rewrite -addnA (subnKC (ltnW h)) addnn. have hb: (n + k).+1 + (n - k - 1) = n.*2. by rewrite - subnDA addn1 - addnS - addnA (subnKC h) addnn. set A := 'C(n.*2, n - k). set B := 'C(n.*2, n - k - 1). have Av: A = 'C(n.*2, n + k) by rewrite - ha binom_mn_n ha. have Bv: B = 'C(n.*2, (n + k).+1) by rewrite - hb binom_mn_n hb. move:(mul_Sm_binm_1 (n- k) (n+k) ); rewrite addnC ha - Av - Bv mulnBr => <-. by rewrite - mulnBl (subnBA _ (ltnW h)) addSn -addnA addnn - addnS addKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)