proposition: Lemma csum_Mlele a b a' b': a <=c a' -> b <=c b' -> (a +c b) <=c (a' +c b').
proof: Proof. by move=> aa' bb'; apply: csum_increasing; aww => x xtp; try_lvariant xtp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)