proposition: Lemma ord_prime_prop4 n: ordinalp n -> ord_prime (oopow n) -> indecomposable n.
proof: Proof. move => on [oon nnz opn]; split. by apply: (ord_ne0_pos on) => nz; case: (proj2 nnz); rewrite nz oopow0. move => a b lan lbn abn. move: (opow_Mo_lt lan) (opow_Mo_lt lbn). move => [[op1 _ _] /nesym od1] [[op2 _ _] /nesym od2]. move:(opow_sum OS_omega (proj31_1 lan) (proj31_1 lbn)); rewrite abn => H. by case:(opn _ _ op1 op2 H). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)