proposition: Lemma regular_indecomposable x: regular_ordinal x -> (x = \0o \/ indecomposable x).
proof: Proof. move => [ox rx]; case: (ozero_dichot ox) => xnz; first by left. right; split => // u v [[ou _ _] unx] vx eq. have ov:= proj31_1 vx. case: (ozero_dichot ov) => vnz. move: eq; rewrite vnz osum0r //. case: (oleNgt(cofinality_pr3 ov)). by move: (cofinality_sum ou vnz); rewrite eq rx => <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)