src/HOL/Divides.thy
changeset 63947 559f0882d6a6
parent 63834 6a757f36997e
child 63950 cdc1e59aa513
     1.1 --- a/src/HOL/Divides.thy	Mon Sep 26 07:56:53 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -2310,6 +2310,16 @@
     1.4      by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
     1.5  qed
     1.6  
     1.7 +lemma zmod_trival_iff:
     1.8 +  fixes i k :: int
     1.9 +  shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
    1.10 +proof -
    1.11 +  have "i mod k = i \<longleftrightarrow> i div k = 0"
    1.12 +    by safe (insert mod_div_equality [of i k], auto)
    1.13 +  with zdiv_eq_0_iff
    1.14 +  show ?thesis
    1.15 +    by simp
    1.16 +qed
    1.17  
    1.18  subsubsection \<open>Quotients of Signs\<close>
    1.19