proposition: Theorem rel_prime_div: forall p q r, rel_prime p q -> (r | p) -> rel_prime r q.
proof: Proof. intros p q r H (u, H1); subst. inversion_clear H as [H1 H2 H3]. red; apply Zis_gcd_intro; try apply Z.divide_1_l. intros x H4 H5; apply H3; auto. apply Z.divide_mul_r; auto. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat