proposition: Lemma nat_prime_P a : nat_prime a <-> ord_prime a /\ a <o omega0.
proof: Proof. split. move => h; split; first exact:(nat_prime_p1 h). by move/olt_omegaP: (proj31 h). move => [[ha hb hc] /olt_omegaP aN]. move:(oclt3 CS1 (CS_nat aN) hb) => lt1a. split => // b c bN cN; rewrite - (oprod2_2int bN cN) => av. have anz :=(proj2 (clt_ltT clt_01 lt1a)). case: (equal_or_not b \0c) => bz; first by case: anz;rewrite av bz oprod0l. case: (equal_or_not c \0c) => cz; first by case: anz; rewrite av cz oprod0r. have H b' c': natp b' -> natp c' -> b' <> \0c -> b' = b' *c c' -> c' = \1c. move => b'N c'N b'nz; rewrite cprodC -{1}(cprod1l (CS_nat b'N)) => h. by rewrite (cprod_eq2r b'N NS1 c'N b'nz h). case: (hc _ _ (OS_nat bN) (OS_nat cN) av)=> eq1. move: av; rewrite eq1 (oprod2_2int bN cN) => bb. right; exact:(H b c bN cN bz bb). move: av; rewrite eq1 (oprod2_2int bN cN) cprodC => bb. left; exact:(H _ _ cN bN cz bb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)