proposition: Lemma ordinals_set_normal E (p := inc ^~E) (r:= fun x y => [/\ p x, p y & x <=o y]) (A:= ordinal (ole_on E)) (f:= Lf (ordinals r) A E): (iclosed_set E) -> normal_function f A E.
proof: Proof. move => [pa pb]. move: (proj2 (ordinals_set_iso pa)); rewrite -/f -/A. move => [o1 o2 [[[ff injf] [_ sjf]] sf tf] fincr]. move: (worder_rc_op p) ; rewrite -/r => pc. move: (wordering_ole_pr pa) => [sc sd]. rewrite sd in tf; rewrite ordinal_o_sr in sf. have fi: forall a b, inc a A -> inc b A -> a <o b -> Vf f a <o Vf f b. hnf in fincr; rewrite sf in fincr injf. move => a b asf bsf [lab nab]; split. have: gle (ordinal_o A) a b by move: lab => [_ _ lab]; apply/sub_gleP. by move /(fincr _ _ asf bsf) => /graph_on_P1 []. by move => h; move: (injf _ _ asf bsf h). split => // a aA la. have oA:=(OS_ordinal sc). set F :=(Vfs f a). have asf: sub a (source f) by rewrite sf; apply: (ordinal_transitive oA). have sfe: sub F E by rewrite -tf ; apply:fun_image_Starget1. have nef: nonempty F. exists (Vf f \0o); apply /(Vf_image_P ff asf); exists \0o => //. exact: (proj32 la). have osF:= Os_sub pa sfe. have faE: inc (Vf f a) E by rewrite -tf; Wtac. have suE:= (ord_sup_ub pa faE). have ofa:= (pa _ faE). have bfa : ordinal_ub F (Vf f a). move => t /(Vf_image_P ff asf) [u ua ->]. have uA:= (ordinal_transitive oA aA ua). move /(oltP (proj31 la)): ua => ua. exact: (proj1 (fi _ _ uA aA ua)). have pr1:=(ord_ub_sup ofa bfa). case: (pb _ sfe nef) => H; first by rewrite - H in suE; apply: (oleA suE pr1). rewrite tf in sjf; move: (sjf _ H); rewrite sf; move => [b bA bv]. move: (Os_ordinal oA aA) (Os_ordinal oA bA) => oa ob. case: (oleT_ell oa ob) => ab; first by ue. by move: (fi _ _ aA bA ab); rewrite - bv => /(oleNgt pr1). have sb: osucc b <o a by move /(limit_ordinal_P): la => [ _]; apply. have sbb: inc (osucc b) a by apply /(oltP oa). have osbA:=(ordinal_transitive oA aA sbb). have h:= (fi _ _ bA osbA (oltS ob)). have: inc (Vf f (osucc b)) F by apply/(Vf_image_P ff asf); ex_tac. by move /(ord_sup_ub osF); rewrite bv => /(oltNge h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)