proposition: Lemma ord_prime_p1 a: ord_prime a <-> [\/ ord_ptypeF a, ord_ptypeI a | ord_ptypeL a].
proof: Proof. split; last first. case. + by move /nat_prime_p1. + by move => [p /proj32_1 /succ_pow_omega_prime op ->]. + move => [p op ->];apply:(ord_prime_prop5' op). move => aprime; move: (aprime) => [oa ag1 ap]. move: (olt_ltT olt_01 ag1) => ag0. move: (CNFp_exists ag0) => [p [n [[axb [qa qb /posnat_ordinalp qc]] nN]]]. move: qc; set a2 := (Q (p n));move => [a2nz a2lo]. move: (OS_CNFp1 axb nN);rewrite /CNFpv. set a3 := CNFpv1 p n => oa3. move:(OS_oopow qb); set a1 := oopow _ => oa1. have oa12: ordinalp (a1 *o a2) by apply: (OS_prod2 oa1 (proj32_1 a2nz)). move => af; case: (ap _ _ oa12 oa3 af)=> af1. case:(ap a1 a2 oa1 (proj32_1 a2nz) af1) => aa1; last first. by constructor 1; apply/nat_prime_P; split => //; rewrite aa1. constructor 3. move:aprime;rewrite aa1 /a1 => apr. by move:(indecomp_prop3 (ord_prime_prop4 qb apr)) => [q op ->]; exists q. move: af1; rewrite /a3 => av. clear a2 a2lo a2nz oa12 af a1 oa1 a3 oa3 qa qb. move:n nN axb av; apply:Nat_induction. by rewrite CNFp_0 => _ ea1; case:(proj2 ag1). move => n nN Hrec axn . rewrite (CNFp_r _ nN). move:(OS_CNFp1r axn (NS_succ nN) (cleS nN)). set a1 := (CNFpv1 p n) => oa1. move: (axn _ (cltS nN)) => [_ ax1 ax2]. rewrite /cantor_pmon (CNFp_pr1 ax1 ax2)/CNFp_value1. move: (OS_succ (OS_pow OS_omega (proj32_1 ax1))); set a2 := osucc _ => oa2. move:(OS_nat (proj1 ax2)) => oa3 av. case:(ap _ _ oa1 (OS_prod2 oa2 oa3) av) => av1; last first. case: (ap _ _ oa2 oa3 av1) => av3. by constructor 2; rewrite av3; exists (P (p n)). move/posnat_ordinalp: ax2 =>[ha hb]. by constructor 1; apply/nat_prime_P; split => //; rewrite av3. by apply: Hrec => // i lin; move:(clt_ltT lin (cltS nN))=> /axn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)