proposition: Lemma ord_sincr_cont_propv f x y: limit_ordinal x -> ordinalp y -> function_prop f x y -> (forall a, inc a x -> Vf f a <o Vf f (osucc a)) -> cont_ofn f x -> normal_function f x y.
proof: Proof. move => [ox _ lx] oy fpxy pa pb; split => // a b ax bx ab. move: (proj32_1 ab) => ob; move: b ob ab bx; apply: least_ordinal2 => z sa sc. case: (ordinal_limA sa). - move => -> ha; case: (olt0 ha). - move=> [w ow wz]; rewrite wz; move /oltSleP => xw zx. have wx: inc w x by apply: (ordinal_transitive ox zx); fprops. have hx:= pa _ wx. case: (equal_or_not a 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) wx) hx). - move => lz az zx; move: (lz) => [oz _ lz1]. move: (proj31_1 az) => oa;move: (oltS oa) => soa. rewrite (pb z zx lz). move /limit_ordinal_P: lz=> [_ lz]. move: (lz _ az) => pc; apply: (olt_leT (sc _ pc soa (lx _ ax))). move: fpxy => [fx sf tf]. have zz: sub z (source f) by rewrite sf; apply: (ordinal_transitive ox zx). apply:ord_sup_ub. move => t /(Vf_image_P fx zz) [u uz ->]. apply: (Os_ordinal oy); rewrite - tf; Wtac. by apply /(Vf_image_P fx zz); exists (osucc a) => //; apply/(oltP oz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)