proposition: Lemma Tnk2_div2 n k: k <= n -> (n-k)`! * (n + k + 1)`! * Tnk2 n k = n.*2 `!* (k.*2.+1).
proof: Proof. move => h. have hb: n - k <= n.*2. rewrite -addnn; exact: (leq_trans (leq_subr k n)(leq_addr n n)). rewrite - mulnA addn1 factSr - mulnA - addn1 (Tnk2_div h) 2! mulnA. by move:(bin_fact hb); rewrite mulnC (subnBA _ h) - addnn - addnA addKn => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)