proposition: Lemma bin_small n m : n < m -> 'C(n, m) = 0.
proof: Proof. by rewrite ltnNge -bin_gt0; case: posnP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)