proposition: Theorem rel_prime_mod: forall p q, 0 < q -> rel_prime p q -> rel_prime (p mod q) q.
proof: Proof. intros p q H H0. assert (H1: Bezout p q 1). - apply rel_prime_bezout; auto. - inversion_clear H1 as [q1 r1 H2]. apply bezout_rel_prime. apply Bezout_intro with q1 (r1 + q1 * (p / q)). rewrite <- H2. pattern p at 3; rewrite (Z_div_mod_eq_full p q); ring. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat