src/HOL/IntDiv.thy

   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
     with h have False by (simp add: mult_assoc)}
   hence "n = m * h" by blast
   thus ?thesis by simp
 qed
-
-
-theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-apply (simp split add: split_nat)
-apply (rule iffI)
-apply (erule exE)
-apply (rule_tac x = "int x" in exI)
-apply simp
-apply (erule exE)
-apply (rule_tac x = "nat x" in exI)
-apply (erule conjE)
-apply (erule_tac x = "nat x" in allE)
-apply simp
-done
 
 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
 proof -
   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
   proof -