proposition: Lemma leq_bin2l n1 n2 m : n1 <= n2 -> 'C(n1, m) <= 'C(n2, m).
proof: Proof. by elim: n1 n2 m => [|n1 IHn] [|n2] [|n] le_n12 //; rewrite leq_add ?IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)