proposition: Lemma csum_le2l' a b c : natp a -> cardinalp b -> cardinalp c -> (a +c b) <=c (a +c c) -> b <=c c.
proof: Proof. move => aN cb cc abc. by case: (cleT_el cb cc) => // /(csum_Meqlt aN) /(cleNgt abc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)