proposition: Lemma least_rem_prop x (b:= least_rem x): \0o <o x -> [/\ ordinalp b, is_rem_of x b & forall z, ordinalp z -> is_rem_of x z -> b <=o z].
proof: Proof. move => h; move: (proj32_1 h) => ox. have px: is_rem_of x x. by split => //; exists \0o; [ apply: OS0 | rewrite osum0l]. exact: (least_ordinal4 ox px). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)