proposition: Lemma ord_sincr_cont_propu f u: (forall x, u <=o x -> f x <o f (osucc x)) -> normal_ofu_aux f u -> sincr_ofsu f u.
proof: Proof. move => h hc x y ux xy. move: (proj32_1 xy) => oy. move: y oy xy; apply: least_ordinal2 => z sa sc. case: (ordinal_limA sa). - move => -> ha; case: (olt0 ha). - move=> [w ow wz]; rewrite wz; move /oltSleP => xw. have hx:= (h _ (oleT ux xw)). case: (equal_or_not x w); [by move => -> | move => xnw ]. have: w <o z by rewrite wz;apply: oltS; apply: OS_succr; ue. move /sc => pw; exact: (olt_ltT (pw (conj xw xnw)) hx). - move => lz xz. rewrite (hc z lz (ole_ltT ux xz)). move /limit_ordinal_P: lz => [ _ lz]. have pa:= (lz _ xz); have psx:= (sc _ pa). have hb:= (oltS (proj32 ux)). move: (psx hb) => ha; apply:(olt_leT ha). set E := fun_image _ _. have: ordinal_set E. apply:Os_funI => a /(ointvP sa) [ua az]; exact: (proj31_1 (h _ ua)). move /ord_sup_ub; apply; apply /funI_P; exists (osucc x) => //. apply/ointvP => //; split =>//; apply: (oleT ux (proj1 hb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)