proposition: Lemma least_ordinal5 x (p: property): \0o <o x -> ~(p x) -> let y := least_ordinal (fun z => (~ (\0o <o z -> p z))) x in [/\ ordinalp y, (\0o <o y), ~(p y) & (forall z, inc z (ordinal_interval \1o y) -> p z)].
proof: Proof. move=> ox px. have orx:= proj32_1 ox. pose q z := \0o <o z -> p z. have nq: ~(q x) by move => qx; move:(qx ox). move: (least_ordinal3 orx nq). rewrite /= /q; set y := least_ordinal _ _. move=> [y1 y2 y3]; split => //; first by ex_middle h; case: y2. by move => z/(ointv1 y1) [z1 z2]; apply: y3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)