proposition: Lemma unbounded_non_coll (p:property): (forall x, ordinalp x -> exists2 y, x <=o y & p y) -> non_coll p.
proof: Proof. move => hp [E Ep]. set F := Zo E ordinalp. have ose: ordinal_set F by move => x /Zo_hi. move:(hp _ (OS_succ (OS_sup ose))) => [y [os oy lexy] /Ep yE]. have lyx :=(lexy _ (setU1_1 (\osup F) (\osup F))). by case :(oleNgt (ord_sup_ub ose (Zo_i yE oy))); apply/(oltP oy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)