proposition: Lemma Zrelprime_divides_intro : forall a b p q : Z, Zdivides a p -> Zdivides b q -> Zrelprime p q -> Zrelprime a b.
proof: Proof. intros a b p q Ha Hb; elim Ha; intros x Hx; rewrite <- Hx; elim Hb; intros y Hy; rewrite <- Hy; rewrite (Zmult_comm x a); rewrite (Zmult_comm y b); apply Zrelprime_mult_intro. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)