src/HOL/NumberTheory/Quadratic_Reciprocity.thy

   then have "2 \<le> q - 1" by arith
   then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
   then show ?thesis by auto
 qed
 
+ML {* fast_arith_split_limit := 0; *} (*FIXME*)
+
 lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
     (p * b \<noteq> q * a)"
 proof
   assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
   then have "q dvd (p * b)" by (auto simp add: dvd_def)

     with prems show ?thesis by auto
   qed
   then have p1: "q \<le> -1" by arith
   with q_g_2 show False by auto
 qed
+
+ML {* fast_arith_split_limit := 9; *} (*FIXME*)
 
 lemma (in QRTEMP) P_set_finite: "finite (P_set)"
   using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
 
 lemma (in QRTEMP) Q_set_finite: "finite (Q_set)"