proposition: Lemma Zrelprime_mult_intro : forall a b x y : Z, Zrelprime (a * x) (b * y) -> Zrelprime a b.
proof: Proof. intros a b x y. unfold Zrelprime in |- *. intro H1. apply Zgcd_intro_unfolded; auto with zarith. generalize (Zgcd_nonzero (a * x) (b * y)); rewrite H1; intro H0; elim H0; auto with zarith. intros q Hq. rewrite <- H1. apply Zdiv_gcd_elim; apply Zdivides_mult_elim_rht; tauto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)