proposition: Lemma Zmod_mult_elim_rht : forall m a b c : Z, (m > 0)%Z -> Zrelprime a m -> ((b * a) mod m)%Z = ((c * a) mod m)%Z -> (b mod m)%Z = (c mod m)%Z.
proof: Proof. intros m a b c; rewrite (Zmult_comm b a); rewrite (Zmult_comm c a); apply Zmod_mult_elim_lft. Qed.
imports: CoRN.model.Zmod.ZGcd