proposition: Lemma Zmodeq_mult_compat : forall a b c d : Z, Zmodeq a b -> Zmodeq c d -> Zmodeq (a * c) (b * d).
proof: Proof. intros a b c d Hab Hcd. apply (Zmodeq_trans (b * c)). apply Zmodeq_mult_elim_rht; assumption. apply Zmodeq_mult_elim_lft; assumption. Qed.
imports: CoRN.model.Zmod.ZGcd