--- a/src/HOL/Divides.thy Mon Sep 26 07:56:53 2016 +0200
+++ b/src/HOL/Divides.thy Mon Sep 26 07:56:54 2016 +0200
@@ -2310,6 +2310,16 @@
by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
qed
+lemma zmod_trival_iff:
+ fixes i k :: int
+ shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
+proof -
+ have "i mod k = i \<longleftrightarrow> i div k = 0"
+ by safe (insert mod_div_equality [of i k], auto)
+ with zdiv_eq_0_iff
+ show ?thesis
+ by simp
+qed
subsubsection \<open>Quotients of Signs\<close>