proposition: Lemma osum_Mlele a b c d: a <=o b -> c <=o d -> (a +o c) <=o (b +o d).
proof: Proof. move=> le1 le2; apply: (oleT (osum_Meqle le2 (proj31 le1))). apply:(osum_Mleeq le1 (proj32 le2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)