proposition: Lemma least_ordinal2' (p:property) : (forall b, ordinalp b -> (forall x, inc x b -> p x) -> p b) -> forall a, ordinalp a -> p a.
proof: Proof. move => H; apply:least_ordinal2 => b ob bp; apply:(H _ ob) => x /(oltP ob). exact: bp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)