proposition: Lemma osum_Meqlt a b c: a <o b -> ordinalp c -> (c +o a) <o (c +o b).
proof: Proof. move => /oltP0 [oa ob ab] oc; apply /oltP; fprops. rewrite (osum_rec_def oc ob); apply /setU2_P; right; apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)