proposition: Lemma nat_prime_p1 a : nat_prime a -> ord_prime a.
proof: Proof. move => [aN ag1 ap]. have oag1 := (oclt ag1). apply:ord_prime_prop1; split; [ by apply:OS_nat | exact: oag1 |]. move => b c ob oc av. case: (ozero_dichot ob) => bp. by move: (proj2 (olt_ltT olt_01 oag1)); rewrite av bp oprod0l. case: (ozero_dichot oc) => cp. by move: (proj2 (olt_ltT olt_01 oag1)); rewrite av cp oprod0r. move: (oprod_Mle1 ob cp) (oprod_M1le bp oc); rewrite - av => le1 le2. move/olt_omegaP: aN => asmall. have bN: natp b by apply/olt_omegaP;exact:(ole_ltT le1 asmall). have cN: natp c by apply/olt_omegaP;exact:(ole_ltT le2 asmall). move:av; rewrite(oprod2_2int bN cN) => h; apply: (ap _ _ bN cN h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)