proposition: Lemma Cat_alt n k: k<=n -> Cat (n+k) (n-k) = Tnk2 n k.
proof: Proof. move => h. rewrite /Tnk2 /Cat (subSn (leq_trans (leq_subr k n) (leq_addr k n))) -addnA. by rewrite (subnKC h) (subnBA _ h) - addnA !addnn addKn addn1 bin_subnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)