proposition: Lemma normal_fn_unbounded f a x: normal_function f a a -> x<o a -> x <=o (Vf f x) /\ Vf f x <o a.
proof: Proof. move=> [[ff sf tf] finc _] laxx. have [[ox oa _ ] _] := laxx. move: x ox laxx; apply: least_ordinal2 => x ox xp lxa. have xsf: inc x a by apply /(oltP oa). have ft: inc (Vf f x) a by Wtac. have ft2: Vf f x <o a by apply/(oltP oa). split => //; case: (oleT_el ox (proj31_1 ft2)) => // lt1. case: (oleNgt (proj1 (xp (Vf f x) lt1 ft2)) (finc (Vf f x) x ft xsf lt1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)