proposition: Lemma least_rem_p0 x: ~(\0o <o x) -> (least_rem x) = \0o.
proof: Proof. move => bad; rewrite /least_rem /least_ordinal; set E := Zo _ _. case: (emptyset_dichot E);first by move ->; rewrite setI_0. move=>[c] /Zo_P [qa [[[_ oc _] /nesym cnz] [b ob xv]]]; case: bad; rewrite xv. case: (ozero_dichot (OS_sum2 ob oc)) => // /(osum2_zero ob oc); case => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)