proposition: Lemma bin_subnn k n: k <= n -> 'C(n.*2, n + k) = 'C(n.*2, n - k).
proof: Proof. move => h; rewrite - bin_sub - addnn ? leq_add2l//. by rewrite -{4} (subnKC h) addnA addKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)