proposition: Lemma indecomp_prop2 a b c: a <o c -> b <o c -> indecomposable c -> a +o b <o c.
proof: Proof. move => ac bc oic. move: (proj31_1 ac) (bc) => oa [[ob oc _] _]. split; last exact: ((proj2 oic) _ _ ac bc). rewrite -(indecomp_prop1 oic ac) -(indecomp_prop1 oic bc) osumA //. apply:(osum_Mle0 (OS_sum2 oa ob) oc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)