proposition: Lemma least_rem_p2 x a b: \0o <o x -> x = a +o b -> ordinalp a -> ordinalp b -> b = \0o \/ least_rem x <=o b.
proof: Proof. move => /least_rem_prop [ha hb hc] xv oa ob. case: (ozero_dichot ob); [by left | move => bp; right; apply: (hc _ ob)]. by split => //; exists a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)