src/HOL/Number_Theory/Gauss.thy

--- a/src/HOL/Number_Theory/Gauss.thy	Wed Jun 19 12:13:16 2024 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Jun 20 14:28:46 2024 +0000
@@ -196,10 +196,7 @@
   by (auto simp add: C_def B_mod_greater_zero)
 
 lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}"
-  apply (auto simp add: F_def E_def C_def)
-   apply (metis p_ge_2 Divides.pos_mod_bound nat_int zless_nat_conj)
-  apply (auto intro: p_odd_int)
-  done
+  using p_ge_2 by (auto simp add: F_def E_def C_def intro: p_odd_int)
 
 lemma D_subset: "D \<subseteq> {x. 0 < x \<and> x \<le> ((p - 1) div 2)}"
   by (auto simp add: D_def C_greater_zero)