src/HOL/Number_Theory/Pocklington.thy
changeset 68157 057d5b4ce47e
parent 67399 eab6ce8368fa
child 68707 5b269897df9d
     1.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sat May 12 17:53:12 2018 +0200
     1.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Sat May 12 22:20:46 2018 +0200
     1.3 @@ -838,7 +838,7 @@
     1.4      {
     1.5        assume "a ^ ((n - 1) div p) mod n = 0"
     1.6        then obtain s where s: "a ^ ((n - 1) div p) = n * s"
     1.7 -        unfolding mod_eq_0_iff by blast
     1.8 +        by blast
     1.9        then have eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
    1.10        from qrn[symmetric] have qn1: "q dvd n - 1"
    1.11          by (auto simp: dvd_def)