proposition: Lemma zdiv_mult_compat_l : forall a b c : Z, ZDivides a b -> ZDivides a (b * c).
proof: Proof. intros. elim H. intro x. intros. unfold ZDivides in |- *. rewrite H0. split with (x * c)%Z. rewrite Zmult_assoc. reflexivity. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp