proposition: Lemma Zmodeq_mult_elim_rht : forall a b c : Z, Zmodeq a b -> Zmodeq (a * c) (b * c).
proof: Proof. intros. rewrite (Zmult_comm a c). rewrite (Zmult_comm b c). apply Zmodeq_mult_elim_lft. assumption. Qed.
imports: CoRN.model.Zmod.ZGcd