proposition: Lemma ordinals_col_p1 (p: property) (f := ordinalsf p): (forall x, p x -> ordinalp x) -> (non_coll p) -> [/\ forall a, ordinalp a -> p (f a), forall x, p x -> exists2 a, ordinalp a & x = f a, forall a b, a<=o b -> (f a) <=o (f b), forall a b, a<o b -> (f a) <o (f b) & (forall a b, ordinalp a -> ordinalp b -> (a<=o b <-> (f a) <=o (f b))) /\ forall a b, ordinalp a -> ordinalp b -> (a<o b <-> (f a) <o (f b))].
proof: Proof. move => pa pb. set r := (fun x y => [/\ p x, p y & x <=o y]). have pc: (non_coll (fun x => r x x)). move => [E Ep]; case: pb; exists E => x; split; first by move /Ep => []. by move => px; apply /Ep; split => //; move: (pa _ px) => /oleR. move: (worder_rc_op p) => pd. have le0: forall a, ordinalp a -> p (f a). by move => a oa; move: (ordinals_Mle pd pc (oleR oa)) => []. have lt1: forall a b, a <o b -> (f a) <o (f b). by move => a b h; move: (ordinals_Mlt pd pc h) => [[_ _]]. have le1: forall a b, a<=o b -> (f a) <=o (f b). by move => a b h; move: (ordinals_Mle pd pc h) => [_ _]. have lt2:forall x, p x -> exists2 a, ordinalp a & x = f a. move => x px. have h: r x x by split => //; move: (pa _ px) => /oleR ox. move:(ordinalsrP pd h) (OS_ordinalr pd h); rewrite -/r -/f => h1 h2. by exists (ordinalr r x). split => //; split. move => a b oa ob; split => h; first by apply: le1. by case: (oleT_el oa ob) => // /lt1 /(oleNgt h). move => a b oa ob; split => h; first by apply: lt1. by case: (oleT_el ob oa) => // /le1 /(oltNge h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)