proposition: Lemma normal_function_equiv f a b X: ordinalp a -> ordinalp b -> normal_function f a b -> sub X a -> nonempty X -> (\osup X = a \/ Vf f (\osup X) = \osup (Vfs f X)).
proof: Proof. move => oa ob h. have incf:= (normal_function_incr oa ob h). move: h => [[ff sf tf] pa pb] Xa nex. have osx:= Os_sub (Os_ordinal oa) Xa. set y := \osup X. case: (equal_or_not y a) => eya; [by left | right]. have lya: y <o a by split => //; apply: ord_ub_sup => // x /Xa /(oltP oa) []. have iya: inc y a by apply /(oltP oa). have ofy: ordinalp (Vf f y) by apply: (Os_ordinal ob); Wtac. have Xsf: sub X (source f) by ue. have osi: ordinal_set (Vfs f X). move =>t /(Vf_image_P ff Xsf) [u uX ->];apply: (Os_ordinal ob); Wtac. case: (inc_or_not y X) => iyX. apply: oleA; last first. apply:ord_ub_sup => // t /(Vf_image_P ff Xsf) [u uX ->]. by apply: incf => //; apply: ord_sup_ub. apply:ord_sup_ub => //; apply /(Vf_image_P ff Xsf); ex_tac. case: (ord_sup_inVlimit osx nex); rewrite -/y => // limy. rewrite (pb _ iya limy). have ysf: sub y (source f) by rewrite sf; move: lya => [[_ _ h] _]. have Xy: sub X y by move => t tX; case/oltP0:(ord_sup_sub osx iyX tX). symmetry; apply: ord_sup_1cofinal; first split. - move => t /(Vf_image_P ff Xsf) [u /Xy ux ->]; apply/(Vf_image_P ff ysf). ex_tac. - move => t /(Vf_image_P ff ysf) [u /(oltP (proj31 limy)) uy ->]. move: (olt_sup osx uy) => [z zx uz]. have h: inc (Vf f z) (Vfs f X) by apply/(Vf_image_P ff Xsf); ex_tac. have /(oltP oa) za:= (Xa _ zx). ex_tac; apply: (incf _ _ (proj1 uz) za). - move =>t /(Vf_image_P ff ysf) [u uX ->];apply: (Os_ordinal ob); Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)