src/HOL/Int.thy
changeset 64849 766db3539859
parent 64758 3b33d2fc5fc0
child 64996 b316cd527a11
     1.1 --- a/src/HOL/Int.thy	Mon Jan 09 18:53:06 2017 +0100
     1.2 +++ b/src/HOL/Int.thy	Mon Jan 09 18:53:20 2017 +0100
     1.3 @@ -357,7 +357,6 @@
     1.4    then show ?thesis ..
     1.5  qed
     1.6  
     1.7 -
     1.8  end
     1.9  
    1.10  text \<open>Comparisons involving @{term of_int}.\<close>
    1.11 @@ -848,6 +847,13 @@
    1.12      by simp
    1.13  qed (auto elim!: Nats_cases)
    1.14  
    1.15 +lemma (in idom_divide) of_int_divide_in_Ints: 
    1.16 +  "of_int a div of_int b \<in> \<int>" if "b dvd a"
    1.17 +proof -
    1.18 +  from that obtain c where "a = b * c" ..
    1.19 +  then show ?thesis
    1.20 +    by (cases "of_int b = 0") simp_all
    1.21 +qed
    1.22  
    1.23  text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
    1.24