proposition: Lemma Zmodeq_gcd_compat_rht : forall a b : Z, Zmodeq a b -> Zgcd a m = Zgcd b m.
proof: Proof. intros. rewrite (Zgcd_symm a m). rewrite (Zgcd_symm b m). apply Zmodeq_gcd_compat_lft. assumption. Qed.
imports: CoRN.model.Zmod.ZGcd