proposition: Lemma ord_prime_prop5 n: indecomposable n -> ord_prime (oopow n).
proof: Proof. move => idn. move:(proj1 idn) => np. move:(proj32_1 np) => on. have oon:= (OS_pow OS_omega on). move:(opow_Mo_lt np); rewrite oopow0 => oogt1. split => // b c ob oc fb. case: (ozero_dichot ob) => bp. by move: (proj2 (olt_ltT olt_01 oogt1)); rewrite fb bp oprod0l. case: (ozero_dichot oc) => cp. by move: (proj2 (olt_ltT olt_01 oogt1)); rewrite fb cp oprod0r. case: (ordinal_limA oc)=> limc; first by case: (proj2 cp). by left; move: (proj1 (ord_prime_prop2 bp cp limc on (esym fb))). case: (ord_prime_prop3 bp limc on (esym fb)). set d := odegree b; move => ha ->. move: (odiff_pr ha) => [oe ev]. case:(indecomp_pr (proj31 ha) oe idn (esym ev)); last by move => ->; right. move => dn; left. apply: oleA; first by move: (proj1 (the_cnf_p4 bp)); ue. by rewrite fb; apply:(oprod_Mle1 ob cp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)