proposition: Lemma iclosed_col_fs (p: property) (f := ordinalsf p) a (x:= f a) (y := f (osucc a)) : (iclosed_proper p) -> ordinalp a -> [/\ x <o y, p x, p y & (forall z, p z -> x <o z -> y <=o z)].
proof: Proof. move => [[pa pb] pc] oa. 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]]. have ob:=(OS_succ oa). move: (s4 _ _ (oltS oa)) => h; split => //; try apply: s1 => //. move => z /s2 [c oc -> fc]. by apply/(s5 (osucc a) c ob oc) /oleSltP /(s6 _ _ oa oc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)