proposition: Lemma indecomp_pr c a b: ordinalp a -> ordinalp b -> indecomposable c -> a +o b = c -> (a = c \/ b = c).
proof: Proof. move => oa ob [_ oix] xs. move: (osum_M0le oa ob)(osum_Mle0 oa ob). rewrite xs => h1 h2. case: (equal_or_not a c)=> lt2; first by left. case: (equal_or_not b c)=> lt1; first by right. by move: (oix _ _ (conj h2 lt2) (conj h1 lt1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)