proposition: Lemma least_rem_p3 x: \0o <o x -> indecomposable (least_rem x).
proof: Proof. move => xp; move: (least_rem_p1 xp) => [lp [a oa av]]. split => // u v lub lvb eq. move: (proj31_1 lub) (proj31_1 lvb) => ou ov. move: av; rewrite - eq (osumA oa ou ov)=> eq1. case:(least_rem_p2 xp eq1 (OS_sum2 oa ou) ov) => dv. by case: (proj2 lub); rewrite - eq dv (osum0r ou). by case: (oltNge lvb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)