proposition: Lemma Zdivides_mult_elim : forall a b c d : Z, Zdivides a b -> Zdivides c d -> Zdivides (a * c) (b * d).
proof: Proof. intros a b c d H1 H2. unfold Zdivides in H1; elim H1; intros q1 H1_. unfold Zdivides in H2; elim H2; intros q2 H2_. exists (q1 * q2)%Z. rewrite <- H1_. rewrite <- H2_. rewrite Zmult_assoc. rewrite Zmult_assoc. rewrite <- (Zmult_assoc q1 q2 a). rewrite (Zmult_comm q2 a). rewrite Zmult_assoc. reflexivity. Qed.
imports: CoRN.model.Zmod.ZBasics