proposition: Lemma osum_Meqle a b c: a <=o b -> ordinalp c -> (c +o a) <=o (c +o b).
proof: Proof. move => ab oc. case: (equal_or_not a b) => nab. by rewrite nab; apply: oleR; apply: (OS_sum2 oc (proj32 ab)). exact: (proj1 (osum_Meqlt (conj ab nab) oc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)