proposition: Lemma indecomp_enum: oopow =1o ordinalsf indecomposable.
proof: Proof. set p := indecomposable. have opp: ordinal_prop p by move => x [/proj32_1 h _]. have p4 :(iclosed_collection p) by split => // F fl nef; apply: indecomp_sup. move:ole_2omega OS_omega => oo odo. have p5: (non_coll p). apply:unbounded_non_coll => // x ox; exists(omega0 ^o x). apply: (opow_Mspec oo ox). by apply: indecomp_prop4. apply:(normal_ofs_uniqueness (p:= fun z => z *o omega0)). - apply: (opow_normal oo). - by apply: (ordinals_col_p2 (conj p4 p5)). - by move => x ox; rewrite oopow_succ. - move => x /(iclosed_col_fs (conj p4 p5)). set u := ordinalsf p x; set v := ordinalsf p (osucc x). move => [uv pu pv h]; move: uv h; move/indecomp_prop3:pu => [a oa ->]. move/indecomp_prop3:pv => [b ob ->] /(opow_Meqltr oo oa ob) => lab h. rewrite - (opow_succ odo oa); ex_middle bad. have ra := (opow_Meqlt oo (oltS oa)). have rb := (indecomp_prop4 (OS_succ oa)). move /(opow_Meqltr oo ob (OS_succ oa)):(conj (h _ rb ra) bad). by move /oltSleP => /(oltNge lab). - move: (iclosed_col_f0 (conj p4 p5)); set u := ordinalsf p \0o. rewrite oopow0; move => [[/oge1P up _] h]. apply:oleA => //; exact: (h _ indecomp_one). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)