proposition: Lemma succ_pow_omega_irred p: ordinalp p -> ord_sprime (osucc (oopow p)).
proof: Proof. move => op; split. exact: (OS_succ (OS_pow OS_omega op)). by rewrite - (osucc_zero); apply/ oltSSP; apply:(oopow_pos op). move => a b oa ob sab. have oop:= OS_pow OS_omega op. have: osuccp (a *o b) by rewrite - sab; exists (omega0 ^o p). move/(oprod_succP oa ob) => [[a1 oa1 av] [b1 ob1 bv]]. have oab1 := (OS_prod2 oa ob1). move: sab. rewrite bv (oprod2_succ oa ob1) {2} av - (osum2_succ oab1 oa1). move/(osucc_inj oop (OS_sum2 oab1 oa1)) => /esym eq1. case: (ozero_dichot ob1) => b1p; first by rewrite b1p osucc_zero; right. case: (indecomp_pr oab1 oa1 (indecomp_prop4 op) eq1) => eq2. rewrite eq2 in eq1; move: (osum2_a_ab oop oa1 eq1) => a1z. by left; rewrite av a1z osucc_zero. move:(oleT (oprod_Mle1 oa b1p) (osum_Mle0 oab1 oa1)). rewrite eq1 -/(oopow _) - eq2 av; case/oleNgt; exact:(oltS oa1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)