proposition: Lemma iclosed_col_f0 (p: property) (f := ordinalsf p) (x:= f \0o): (iclosed_proper p) -> (p x /\ (forall z, p z -> x <=o z)).
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; first by apply: s1; fprops. by move => z /s2 [a /ole0x oa ->]; apply: s3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)