src/ZF/Integ/IntDiv.thy

  prefer 2
  apply (subst int_succ_int_1)
  apply (erule natE)
 apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def)
 apply (frule nat_0_le)
-apply (erule (1) notE impE)
 apply (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j) ")
 apply (simp (no_asm_use))
 apply (rule zadd_zless_mono)
 apply (simp_all (no_asm_simp) add: zle_def)
 done

          q \<in> int; q' \<in> int;  
          r \<in> int; r' \<in> int |] ==> r = r'"
 apply (subgoal_tac "q = q'")
  prefer 2 apply (blast intro: unique_quotient)
 apply (simp add: quorem_def)
-apply auto
 done
 
 
 subsection{*Correctness of posDivAlg, 
            the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"} *}