proposition: Lemma Nprime_le_rel_prime : forall n p, Nprime p -> 0 < n < p -> Nrel_prime n p.
proof: Proof. intros. destruct H0. destruct H. intro. intros. assert (0<n0). apply Ndiv_non_0 with n. auto. auto with arith. assert (n0<p). apply Nat.le_trans with (S n). apply le_n_S. apply Ndiv_le. auto with arith. trivial. auto. destruct n0. apply Ndiv_0_n in H3. rewrite H3 in H0. inversion H0. destruct n0. trivial. apply H2 in H4. contradiction. split. auto with arith. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)