proposition: Lemma least_ordinal1 x (p: property) (y:= least_ordinal p x) : ordinalp x -> p x -> [/\ ordinalp y, p y & forall z, ordinalp z -> p z -> sub y z].
proof: Proof. move=> ox px. set (t:= Zo (osucc x) p). have xt: inc x t by apply :Zo_i; fprops. have net: nonempty t by exists x. have osbx:= (OS_succ ox). have alo: (ordinal_set t) by apply:(Os_sub (Os_ordinal osbx)); apply: Zo_S. have h:= (ordinal_setI net alo). split;[by apply: alo | by move: h => /Zo_hi | move=> z oz pz ]. have aux: inc z t -> sub y z by move=> zt w wi; apply: (setI_hi wi zt). case: (ordinal_inA ox oz) => ty. - exact: (sub_trans (setI_s1 xt) (ordinal_transitive oz ty)). - by apply: aux; apply: Zo_i => //;apply: setU1_r. - apply: aux; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)