proposition: Lemma divmultgcd : forall a b c : Z, a <> 0%Z -> ZDivides a (b * c) -> gcd a b 1 -> ZDivides a c.
proof: Proof. intros. elim (gcd_lincomb a b 1). intro alpha. intros. elim H2. intro beta. intros. elim H0. intro y. intros. split with (c * alpha + y * beta)%Z. rewrite Zmult_plus_distr_r. rewrite Zmult_assoc. rewrite Zmult_assoc. rewrite <- H4. rewrite (Zmult_comm a c). rewrite (Zmult_comm b c). rewrite Zmult_assoc_reverse. rewrite Zmult_assoc_reverse. rewrite <- Zmult_plus_distr_r. transitivity (c * 1)%Z. rewrite Zmult_comm. rewrite Zmult_1_l. reflexivity. apply (f_equal (A:=Z)). assumption. assumption. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo gcd