proposition: Lemma T_nkbin_pr n k : n.*2.+1 * 'C(n+k,k.*2) = (k.*2.+1) * (T_nkbin n k).
proof: Proof. rewrite /T_nkbin binS addnA addnn - (muln2 'C(_, _)) mulnDr mulnA. rewrite - mul_Sm_binm_2 (mulnC _ 2) mulnA - mulnDl addnS -{3} (mul2n k). rewrite - mulnDr -(addnn k) subnDA addnK - mul2n. case (leqP k n) => h; rewrite ?(subnK h) // bin_small ? ltn_add2r ?muln0 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)