proposition: Lemma sum_monotony (a1 := \1o)(b1:= omega0) (a2 := omega0 *o \2o)(b2:= omega0 *o (osucc \2o)) (a3 := omega0)(b3:= omega0 +o \1o): [/\ a1 <o b1 /\ a1 +o b1 <o b1 +o a1, a2 <o b2 /\ a2 +o b2 = b2 +o a2 & a3 <o b3 /\ b3 +o a3 <o a3 +o b3 ].
proof: Proof. have ha := olt_1omega. have hb := OS_omega. have hc := olt_0omega. have hd := (OS_succ OS2). have he := (OS_sum2 hb hb). split; split. - done. - by rewrite (osum_int_omega ha) (osucc_pr hb); apply: oltS. - apply: (oprod_Meqlt (oltS OS2) hc). - rewrite - (oprodD OS2 hd hb) - (oprodD hd OS2 hb) - (succ_of_nat NS2). by rewrite (osum2_2int NS2 NS3) (osum2_2int NS3 NS2) csumC. - by rewrite /a3/b3 (osucc_pr hb); apply: oltS. - rewrite /a3/b3 (osumA hb hb OS1) (osucc_pr he). by rewrite - (osumA hb OS1 hb) (osum_int_omega ha); apply: (oltS he). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)