proposition: Lemma csum_lt2l' 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 nac]. split;[ apply: (csum_le2l' aN cb cc abc) | dneg bc; ue]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)