proposition: Lemma indecomp_prop4 y: ordinalp y -> indecomposable (oopow y).
proof: Proof. move: y;apply: least_ordinal2 => z oz zle. case:(ordinal_limA oz)=> zl. rewrite zl oopow0; exact indecomp_one. move: zl => [x ox zv]. rewrite zv (oopow_succ ox). apply/(indecomp_prodP olt_1omega (oopow_pos ox));apply: indecomp_omega. rewrite /oopow (proj2 (opow_normal (ole_2omega)) _ zl). set E := (fun_image z oopow). have pa: (forall x, inc x E -> indecomposable x). by move => x /funI_P [t /(oltP oz) tz ->]; apply: zle. apply:(indecomp_sup pa); exists \1o; apply/funI_P. by exists \0o; [exact (proj32 zl) | rewrite oopow0 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)