proposition: Lemma least_rem_p7 a b: ordinalp a -> \0o <o b -> least_rem (a+o b) = least_rem b.
proof: Proof. move => oa bp. move:(least_rem_p1 bp)(least_rem_p3 bp); set c := least_rem b. move =>[cp [u ou bv]] ic. have oc := proj32_1 cp. have ha: is_rem_of (a +o b) c. by split => //; exists (a +o u); fprops; rewrite - (osumA oa ou oc) - bv. by move:(least_rem_p6 (ord_gt_pos (osum_Meqlt bp oa)) ha ic). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)