proposition: Lemma Tnk1_eq_Tnk2 n k: k+2 <=n -> Tnk1 n k = Tnk2 n k.
proof: Proof. move => h. set m := (n - k).-2. move:(subnK h); rewrite subnDA subn2 -/m => nv. have nk2: n - k = m.+2 by rewrite - nv (addnC k) addnA addn2 addnK. rewrite /Tnk1 /Tnk2 {1 3} nk2 - {1 2 4 5}nv -/m addn2 addnS doubleS /=. rewrite -addnA addn1 addSn - addnA addnn doubleS - addnS. have h1: 0 < (m + k.*2.+3) by rewrite addnS. apply/eqP; rewrite - (eqn_pmul2l h1). by move/andP:( catalan_spec m k) => [hh /eqP <-]; rewrite (mulKn _ h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)