proposition: Lemma osum_increasing5 u f: ordinalp u -> (sincr_ofsu f u) -> ((forall x y, u <=o x -> ordinalp y -> f(x) +o y <=o f (x +o y)) /\ (exists2 c, u <=o c & forall x, c <=o x -> x <=o f (x))).
proof: Proof. move=> ou h. have osw:= (ofs_sincru h). set goal1 := (forall x, _). have pr1:goal1. move=> x y ux oy. have ox:= proj32 ux. move: y oy; apply: least_ordinal2 => z oz hr. have owx:= (osw _ ux). have pa t: ordinalp t -> u <=o (x +o t). move=> ot;exact: (oleT ux (osum_Mle0 ox ot)). have pb t: t <o z -> f x +o t <o f (x+o z). move => ltz; apply: (ole_ltT (hr t ltz)). exact: (h _ _ (pa _ (proj31_1 ltz)) (osum_Meqlt ltz ox)). case: (ordinal_limA oz). - move=> ->; rewrite (osum0r ox)(osum0r owx); apply:(oleR owx). - move=> [t ot uv]. move: (oltS ot); rewrite -uv => h1. rewrite {1} uv -(osum2_succ owx ot); apply /oleSltP; apply: (pb _ h1). - move: (osum_normal owx) => [_ opn]. move=> lz; rewrite (opn _ lz). apply: ord_ub_sup; first by apply: osw; apply: pa. move=> i /funI_P[j jz ->]. have ljz: j <o z by apply /oltP. exact:(proj1 (pb _ ljz)). split; first by exact. set b:= osucc u. have ob: ordinalp b by apply: OS_succ. move: (oltS ou); rewrite -/b; move => [leab _]. set c := b *o omega0. have ab:= (oleT leab (oprod_Mle1 ob olt_0omega)). exists c; first by exact. suff bv: c <=o f c by move => x xc; apply: (osi_gexu h ab bv xc). have bp: \0o <o b by apply: (olt0S ou). have [_ aux] := (oprod_normal bp). move: (aux _ omega_limit); rewrite - /c => e1; rewrite {1} e1. have owc: ordinalp (f c) by apply:osw. have H: forall z, inc z omega0 -> ordinalp (b *o z). move => z zo;exact: (OS_prod2 ob (OS_nat zo)). apply: ord_ub_sup => // t /funI_P[z zo ->]; move:(H _ zo) => obz //. have owb: ordinalp (f b) by apply: osw. have oz := (OS_nat zo). have le1: b *o z <=o (f b +o (b *o z)) by apply: osum_M0le. move: (pr1 _ _ leab obz);rewrite (oprod2_nsucc ob oz) => le2. have le3:= (oleT le1 le2). have ltno: (\1o +o z) <o omega0. apply: osum2_lt_omega; [apply :olt_1omega | by apply/(oltP OS_omega) ]. have le5: u <=o (b *o (\1o +o z)). by rewrite -(oprod2_nsucc ob oz); apply: (oleT leab); apply: osum_Mle0. exact: (oleT le3(proj1 (h _ _ le5 (oprod_Meqlt ltno bp)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)