src/HOL/Library/Target_Numeral.thy

   have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0"
     by (auto simp add: sgn_if)
   have aux2: "\<And>q::int. - int_of k = int_of l * q \<longleftrightarrow> int_of k = int_of l * - q" by auto
   show ?thesis
     by (simp add: prod_eq_iff Target_Numeral.int_eq_iff prod_case_beta aux1)
-      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if zdiv_zminus2 zmod_zminus2 aux2)
+      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
 qed
 
 lemma div_int_code [code]:
   "k div l = fst (divmod k l)"
   by simp