proposition: Lemma least_rem_p4 x b : indecomposable x -> is_rem_of x b -> b = x.
proof: Proof. move => ix [lp [a oa xv]]. case: (indecomp_pr oa (proj32_1 lp) ix (esym xv)) => // eax. by move: (osum_Meqlt lp oa); rewrite (osum0r oa) - xv eax; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)