proposition: Lemma Zmodeq_mult_elim_lft : forall a b c : Z, Zmodeq a b -> Zmodeq (c * a) (c * b).
proof: Proof. intros. unfold Zmodeq in |- *. unfold Zminus in |- *. rewrite (Zmult_comm c b). rewrite <- Zopp_mult_distr_l_reverse. rewrite (Zmult_comm c a). rewrite <- Zmult_plus_distr_l. fold (a - b)%Z in |- *. apply Zdivides_mult_elim_rht. assumption. Qed.
imports: CoRN.model.Zmod.ZGcd