proposition: Lemma csum_Mlelt a b a' b': natp a' -> a <=c a' -> b <c b' -> (a +c b) <c (a' +c b').
proof: Proof. move=> a'N aa' bb'. exact: (cle_ltT (csum_Mleeq b aa') (csum_Meqlt a'N bb')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)