proposition: Lemma ord_sincr_cont_prop f: (forall x, ordinalp x -> f x <o f (osucc x)) -> normal_of_aux f -> sincr_ofs f.
proof: Proof. move => pa pb. have pa1: (forall x, \0o <=o x -> f x <o f (osucc x)). by move => x [_ ox _]; apply: pa. have pa2: (forall x, limit_ordinal x -> \0o <o x -> f x = \osup (fun_image (ordinal_interval \0o x) f)). move => x lx; move: (lx) => /pb -> _; rewrite ointv_pr1 //;exact:(proj31 lx). move => x y xy. exact: (ord_sincr_cont_propu pa1 pa2 (ole0x (proj31_1 xy)) xy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)