proposition: Lemma Zmod_mult_elim_lft : forall m a b c : Z, (m > 0)%Z -> Zrelprime a m -> ((a * b) mod m)%Z = ((a * c) mod m)%Z -> (b mod m)%Z = (c mod m)%Z.
proof: Proof. intros m a b c Hm Hrelprime Hmulteq. assert (Hm0 : m <> 0%Z); auto with zarith. generalize (Zdivides_Zmod0 _ _ Hm0 (Zmod_minus_elim m _ _ Hm Hmulteq)); intro Hdiv. rewrite (Zmult_comm a b) in Hdiv; rewrite (Zmult_comm a c) in Hdiv; rewrite <- BinInt.Zmult_minus_distr_r in Hdiv. apply Zmod_minus_intro; auto. apply Zmod0_Zdivides. auto with zarith. apply (Zrelprime_div_mult_intro m a (b - c)). apply Zrelprime_symm; assumption. rewrite Zmult_comm; assumption. Qed.
imports: CoRN.model.Zmod.ZGcd