proposition: Lemma OS_least_rem x: ordinalp (least_rem x).
proof: Proof. case: (p_or_not_p (\0o <o x)) => h. by case (least_rem_prop h). rewrite (least_rem_p0 h); apply: OS0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)