proposition: Lemma indecomp_prop3 x: indecomposable x -> exists2 y, ordinalp y & x = oopow y.
proof: Proof. move=> oidx. move:(ord_ext_div_exists (ole_2omega) (proj1 oidx)) => [a [b [c]]]. move => [oa ob oc [pa pb pc pd]]. symmetry in pa. have op:= proj32_1 pb. move: (olt_leT pb (oprod_Mle1 op pd)) => lt1. have op1:= (proj32_1 lt1). case: (indecomp_pr op1 oc oidx pa) => eq1; last first. by move: (proj2 (olt_leT lt1 (osum_Mle0 op1 oc))); rewrite pa eq1. have bN: natp b by exact (olt_i pc). have bz:= nesym (proj2 pd). move: (cpred_pr bN bz)=> []; set b1:= cpred b. move => ra;rewrite (succ_of_nat ra) => rb. move:(OS_nat ra) => ob1;move: (OS_prod2 op ob1) => h2. move: eq1; rewrite rb (oprod2_succ op ob1) => h1. case:(indecomp_pr (OS_prod2 op ob1) op oidx h1) => eq2. by case: (oopow_nz oa);move:(osum2_a_ab h2 op); rewrite h1;apply. by exists a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)