proposition: Lemma Zdivides_mult_ll : forall a b c d : Z, (a * b)%Z = (c * d)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.
proof: Proof. intros a b c d Heq Ha Hdiv. elim Hdiv; intros x Hx. rewrite <- Hx in Heq. exists x. apply (Zmult_intro_lft a). assumption. rewrite Heq. rewrite Zmult_assoc. rewrite (Zmult_comm x a). auto. Qed.
imports: CoRN.model.Zmod.ZBasics