proposition: Lemma Zrelprime_mult_div_simpl : forall a b x y : Z, Zrelprime a b -> (x * a)%Z = (y * b)%Z -> Zdivides b x.
proof: Proof. intros a b x y Hab Heq. case (Zdec a). intro Ha; rewrite Ha in Hab; unfold Zrelprime in Hab; rewrite Zgcd_zero_lft in Hab. exists (Z.sgn b * x)%Z; rewrite Zmult_comm; rewrite Zmult_assoc; rewrite (Zmult_comm b (Z.sgn b)); rewrite <- Zmult_sgn_eq_abs; rewrite Hab; apply Zmult_1_l. intro Ha. apply (Zmult_div_simpl_3 a x y b Heq Ha). apply (Zrelprime_div_mult_intro a b y Hab). exists x. rewrite Heq; apply Zmult_comm. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)