proposition: Lemma indecomp_prop1 c a: indecomposable c -> a <o c -> a +o c = c.
proof: Proof. move=> [_ oi] ltac; move: (ltac) =>[leac _]. move: (odiff_pr leac) => [_ se]. case: (ole_eqVlt (odiff_Mle (proj31 leac) (proj32 leac))) => h. by rewrite {2} se h. by move: (oi _ _ ltac h); rewrite - se. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)