proposition: Lemma least_ordinal4 x (p: property) (y := least_ordinal p x): ordinalp x -> p x -> [/\ ordinalp y, p y & (forall z, ordinalp z -> p z -> y <=o z) ].
proof: Proof. move=> ox px; move: (least_ordinal1 ox px) => [p1 p2 p3]. split => // t ot pt;move: (p3 _ ot pt) => zt; hnf;split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)