proposition: Lemma least_ordinal3 x (p: property) (y := least_ordinal (fun z => (~ p z)) x): ordinalp x -> ~ (p x) -> [/\ ordinalp y, ~(p y) & (forall z, z <o y -> p z)].
proof: Proof. move=> ox px. move: (least_ordinal4 (p:= (fun z => ~ p z)) ox px) => [p1 p2 p3]. split => // z zy. by ex_middle npz; move: (p3 _ (proj31_1 zy) npz) => /(oltNge zy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)