proposition: Lemma rel_prime_mult : forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c).
proof: Proof. intros a b c Hb Hc. elim (rel_prime_bezout a b Hb); intros u v H. elim (rel_prime_bezout a c Hc); intros u0 v0 H0. apply bezout_rel_prime. apply (Bezout_intro _ _ _ (u * u0 * a + v0 * c * u + u0 * v * b) (v * v0)). rewrite <- H. replace (u * a + v * b) with ((u * a + v * b) * 1); [ idtac | ring ]. rewrite <- H0. ring. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat