proposition: Theorem Nrel_prime_mod : forall a b r, Nrel_prime a b -> Nmod a b r -> Nrel_prime a r.
proof: Proof. intros. destruct H0. unfold Nrel_prime in H. unfold Nrel_prime. intros. assert (n|b). rewrite H0. apply Ndiv_plus_compat. rewrite Nat.mul_comm. apply Ndiv_mult_compat. auto. auto. apply H. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)