proposition: Lemma regular_indecomposable1 x: regular_ordinal x -> [\/ x = \0o, x= \1o, x =omega0 | exists2 y, limit_ordinal y & x = omega0 ^o y].
proof: Proof. move=> rx; case: (regular_indecomposable rx) => ix; first by constructor 1. move: (indecomp_prop3 ix) rx => [y oy ->] [_ ha]. case: (ordinal_limA oy) => h; first by rewrite h oopow0; constructor 2. move: h => [t ot st]. move: OS_omega => oo. move: (OS_oopow ot) (oopow_pos ot) => op tbz. move: (cofinality_prod_omega tbz); rewrite - (opow_succ oo ot) - st ha. by move => hb;constructor 3. by constructor 4; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)