proposition: Lemma Nnon_rel_prime_n_n : forall n, n <> 1 -> ~(Nrel_prime n n).
proof: Proof. intro. intro. intro. unfold Nrel_prime in H0. assert (n=1). apply H0. apply Ndiv_n_n. apply Ndiv_n_n. contradiction. Qed.
imports: Coq(Arith Euclid Compare Lia)