proposition: Lemma least_ordinal0 E (x:= intersection E): ordinal_set E -> nonempty E -> [/\ ordinalp x, inc x E & forall y, inc y E -> x <=o y].
proof: Proof. move => sa sb. have xe:= (ordinal_setI sb sa). have ox:=(sa _ xe). split => // y yE;split;[ exact | exact (sa _ yE)| exact:(setI_s1 yE)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)