proposition: Lemma binom_exchange1 j k n: 'C(j+n,j+k) * 'C(j+k,j) = 'C(n,k) * 'C(j+n,j).
proof: Proof. case: (ltnP n k) => nk; last by rewrite - (subnKC nk) addnA binom_exchange. by rewrite (bin_small nk) bin_small ?mul0n // ltn_add2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)