proposition: Lemma indecompP c: \0o <o c -> (indecomposable c <-> (forall a, a <o c -> a +o c = c)).
proof: Proof. move => cp; split; first by move => /indecomp_prop1. move=> h; split=> // a b lt1 [lt2 ne2]. rewrite - (h _ lt1) => h1; case: ne2. exact: (osum2_simpl (proj31 lt2) (proj32 lt2) (proj31_1 lt1) h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)