proposition: Lemma ordinals_col_p2 (p: property) (f := ordinalsf p): (iclosed_proper p) -> normal_ofs f.
proof: Proof. move => [[pa pb] pc]. set r := (fun x y => [/\ p x, p y & x <=o y]). move: (ordinals_col_p1 pa pc); rewrite -/r -/f; move => [s1 s2 s3 s4 [s5 s6]]. split=> // a la. have [oa zea lla] := la. set F :=(fun_image a f). have nef: nonempty F by apply: funI_setne; ex_tac. have Fp: (forall x, inc x F -> p x). move => t /funI_P[z za ->]; apply:s1 (Os_ordinal oa za). have osF: ordinal_set F by move => t /Fp/pa. move: (pb _ Fp nef) => puF. have bfa : ordinal_ub F (f a). by move => t /funI_P [z /(oltP oa) [za _] ->]; apply:s3. have ofa:= (pa _ (s1 _ oa)). move: (ord_ub_sup ofa bfa). move: (s2 _ puF) => [b ob bv]; rewrite bv => p1. case: (oleT_el oa ob) => cab; first exact :(oleA (s3 _ _ cab) p1). move:(s4 _ _ (oltS ob)) => h. have sb: osucc b <o a by move /(limit_ordinal_P): la => [ _]; apply. have sbb: inc (osucc b) a by apply /(oltP oa). have: inc (f (osucc b)) F by apply/funI_P; ex_tac. by move /(ord_sup_ub osF); rewrite bv=> /(oltNge h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)