proposition: Lemma osum_Mleeq a b c: a <=o b -> ordinalp c -> (a +o c) <=o (b +o c).
proof: Proof. move => ab; move: c; apply: least_ordinal2' => d od H. move: (ab) => [oa ob sab]. split; fprops; move:(OS_sum2 ob od). rewrite (osum_rec_def oa od) (osum_rec_def ob od) => oh t;case /setU2_P. by move => ta; apply/setU2_P; left; apply: sab. move /funI_P => [z zd ->]; apply:(ole_ltT_s oh (H _ zd)). apply/setU2_P; right; apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)