proposition: Lemma Zis_gcd_mult : forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d).
proof: Proof. intros a b c d; intro H; generalize H; simple induction 1. constructor; auto with zarith. intros x Ha Hb. elim (Zis_gcd_bezout a b d H). intros u v Huv. elim Ha; intros a' Ha'. elim Hb; intros b' Hb'. apply Zdivide_intro with (u * a' + v * b'). rewrite <- Huv. replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)). - rewrite Ha'; rewrite Hb'; ring. - ring. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat