proposition: Lemma Zmodeq_relprime : forall a b : Z, Zmodeq a b -> Zrelprime a m -> Zrelprime b m.
proof: Proof. intros a b H. unfold Zrelprime in |- *. rewrite (Zmodeq_gcd_compat_rht a b H). tauto. Qed.
imports: CoRN.model.Zmod.ZGcd