proposition: Lemma indecomp_example x: \0o <o x -> ~ (indecomposable (osucc x)).
proof: Proof. move=> [[_ ox _] xnz'] [_ h2]. have p1:= (oltS ox). have p2:= (ole_ltT (oge1 ox (nesym xnz')) p1). case: (h2 _ _ p1 p2); rewrite osucc_pr //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)