proposition: Lemma Nrel_prime_prime (a p : nat) : Nprime p -> Nrel_prime a p <-> ~ (p | a).
proof: Proof. intros Pp. pose proof Nprime_ge_2 _ Pp as p2. split; intros ap. - intros pa. specialize (ap p pa (Ndiv_n_n _)). lia. - apply Nrel_prime_sym. eapply Nrel_prime_eqmod with (a mod p). lia. now rewrite Nat.mod_mod; lia. apply Nrel_prime_sym, Nprime_le_rel_prime; auto. split. + rewrite (Ndivide_eqmod _ _ (a mod p)) in ap. 2: lia. 2: now rewrite Nat.mod_mod; lia. enough (0 <> a mod p) by lia. intros e. apply ap. rewrite <-e. apply Ndiv_0. + apply Nat.mod_upper_bound. lia. Qed.
imports: Coq(Arith Euclid Compare Lia)