proposition: Lemma Zmult_div_simpl_1 : 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. rewrite (Zmult_comm x a) in Heq. rewrite <- Zmult_assoc in Heq. exists x. apply (Zmult_intro_lft a); auto. Qed.
imports: CoRN.model.Zmod.ZBasics