proposition: Theorem rel_prime_mod_rev: forall p q, 0 < q -> rel_prime (p mod q) q -> rel_prime p q.
proof: Proof. intros p q H H0. rewrite (Z_div_mod_eq_full p q). red. apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat