proposition: Lemma normal_ofs_limit1 f u x: normal_ofs1 f u -> u <o x -> limit_ordinal x -> limit_ordinal (f x).
proof: Proof. move=> /normal_ofs_equiv [pa pb] cux lx. rewrite (pb _ lx cux); move/limit_ordinal_P: (lx) => [[[_ ox _] _] pd]. have ov := (ofs_sincru pa). set E := (fun_image (ordinal_interval u x) f). have ou:= proj31_1 cux; have luu:= (oleR ou). have uu: inc u (ordinal_interval u x) by apply/(ointvP ox). have oe: ordinal_set E. by apply:Os_funI => z /(ointvP ox) [uz _]; apply: ov. have ne: nonempty E by rewrite /E;exists (f u); apply /funI_P;ex_tac. case: (ord_sup_inVlimit oe ne) => //. move=> /funI_P [z /(ointvP ox) [sa /pd sb] fz]. have lt1:= (oltS (proj32 sa)). have se: inc (f (osucc z)) E. apply /funI_P; exists (osucc z)=> //;apply /(ointvP ox). split => //;exact (oleT sa (proj1 lt1)). move: (ord_sup_ub oe se); rewrite fz => l1. case:(oltNge(pa z (osucc z) sa lt1) l1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)