proposition: Lemma indecomp_limit2 n: \0o <o n -> limit_ordinal (oopow n).
proof: Proof. move => [[_ on _] nz]. case: (indecomp_limit (indecomp_prop4 on)) => // pa. case:(opow_eq_one OS_omega on pa) => h; first by case: (proj2 olt_1omega). by case: nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)