proposition: Lemma Nrel_prime_1 : forall n, Nrel_prime n 1.
proof: Proof. intros. intro. intros. destruct n0. destruct H0. rewrite Nat.mul_0_r in H0. auto. apply Ndiv_le in H0. destruct n0. auto. inversion H0. inversion H2. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)