proposition: Lemma least_ordinal2 (p:property) : (forall b, ordinalp b -> (forall x, x <o b -> p x) -> p b) -> forall a, ordinalp a -> p a.
proof: Proof. move => H a oa. case: (p_or_not_p (p a)) => np //. move: (least_ordinal3 oa np). set y := least_ordinal _ _. move => [oy npy Hy]; case: npy => //. by apply: (H _ oy) => x /Hy lxy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)