proposition: Lemma least_int_prop n (p: property) (y:= least_ordinal p n): natp n -> p n -> [/\ natp y, p y& forall z, natp z -> p z -> y <=c z].
proof: Proof. move => nN pn; move: (OS_nat nN) => on. move: (least_ordinal4 on pn) => [ha hb hc]. move: (hc n on pn) => lyn. have yN: natp y. by apply/ (oltP OS_omega); apply: (ole_ltT lyn);apply/ (oltP OS_omega). split => // z zN pz;exact:(ocle3 (CS_nat yN) (CS_nat zN) (hc z (OS_nat zN) pz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)