proposition: Lemma indecomp_limit a: indecomposable a -> a = \1o \/ limit_ordinal a.
proof: Proof. move => oix. have ox:= (OS_indecomposable oix). case:(ordinal_limA ox); last by move=> lx; right. by move: oix => [[_ pa] _] xe; case: pa. move=> [y oy ysx]; left; rewrite ysx. case: (equal_or_not y \0o) => ynz; first by rewrite ynz osucc_zero. by move: (indecomp_example (ord_ne0_pos oy ynz)); rewrite -ysx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)