src/HOL/NumberTheory/Gauss.thy

 
 lemma (in GAUSS) A_res: "ResSet p A"
   apply (auto simp add: A_def ResSet_def)
   apply (rule_tac m = p in zcong_less_eq)
   apply (insert p_g_2, auto)
-  apply (subgoal_tac [1-2] "(p - 1) div 2 < p")
-  apply (auto, auto simp add: p_minus_one_l)
   done
 
 lemma (in GAUSS) B_res: "ResSet p B"
   apply (insert p_g_2 p_a_relprime p_minus_one_l)
   apply (auto simp add: B_def)

   by (auto simp add: D_def C_def B_def A_def)
 
 lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   by (auto simp add: D_eq)
 
+ML {* fast_arith_split_limit := 0; *} (*FIXME*)
+
 lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   apply (auto simp add: F_eq A_def)
 proof -
   fix y
   assume "(p - 1) div 2 < StandardRes p (y * a)"

   also have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1"
     by arith
   finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2"
     using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
 qed
+
+ML {* fast_arith_split_limit := 9; *} (*FIXME*)
 
 lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
   using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
 
 lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1"