proposition: Lemma Zrelprime_div_mult_elim : forall a b c : Z, Zrelprime a b -> Zdivides a c -> Zdivides b c -> Zdivides (a * b) c.
proof: Proof. intros a b c Hab Ha Hb. elim Ha; intros x Hx. elim Hb; intros y Hy. rewrite <- Hx. rewrite (Zmult_comm x a). cut (Zdivides b x); auto with zarith. apply (Zrelprime_mult_div_simpl a b x y Hab). rewrite Hx; rewrite Hy; auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)