src/HOL/Number_Theory/Gauss.thy
changeset 66817 0b12755ccbb2
parent 65435 378175f44328
child 66888 930abfdf8727
     1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -196,7 +196,8 @@
     1.4    moreover have "int y = 0 \<or> 0 < int y" for y
     1.5      by linarith
     1.6    ultimately show "0 < x mod int p"
     1.7 -    by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
     1.8 +    using B_greater_zero [of x]
     1.9 +    by (auto simp add: mod_int_pos_iff intro: neq_le_trans)
    1.10  qed
    1.11  
    1.12  lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}"