proposition: Lemma least_ordinal6 x (p:property) (y :=least_ordinal (fun z => ~ p z) x): ordinalp x -> p x \/ [/\ ordinalp y, forall z, inc z y -> p z & ~ p y].
proof: Proof. move => oc; case: (p_or_not_p (p x)) => np; [by left | right]. move:(least_ordinal3 oc np) => [pa pb pc]; split => // z zy. by apply:pc; apply/(oltP pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)