proposition: Lemma Tnk2_div n k: k <= n -> (n + k + 1) * Tnk2 n k = 'C(n.*2, n-k) * (k.*2.+1).
proof: Proof. rewrite /Tnk2 leq_eqVlt => /orP; case => np. by rewrite (eqP np) addnn addn1 mulnK // mulnC. by rewrite (mulnC _ k.*2.+1) (Tnk2_alt np) addn1 mulKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)