proposition: Theorem Zmod_closeby_eq: forall a b n, 0 <= a -> 0 <= b < n -> a - b < n -> a mod n = b -> a = b.
proof: Proof. intros a b n H H1 H2 H3. case (Zle_or_lt 0 (a - b)); intros H4. case Zle_lt_or_eq with (1 := H4); clear H4; intros H4; auto with zarith. contradict H2; apply Zle_not_lt; apply Zdivide_le; auto with zarith. apply Zmod_divide_minus; auto with zarith. rewrite <- (Zmod_small a n); try split; auto with zarith. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic