proposition: Lemma Zmodeq_small : forall a b c : Z, (0 <= a < c)%Z -> (0 <= b < c)%Z -> Zdivides c (a - b) -> a = b.
proof: Proof. intros a b c Ha Hb Hc. cut ((a - b)%Z = 0%Z); auto with zarith. apply (Zdivisor_small (a - b) c). assumption. apply Zabs_lt_elim; auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics