src/HOL/Number_Theory/Pocklington.thy
changeset 58834 773b378d9313
parent 57514 bdc2c6b40bf2
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -774,8 +774,8 @@
     1.4          unfolding mod_eq_0_iff by blast
     1.5        hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
     1.6        from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
     1.7 -      from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
     1.8 -      have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
     1.9 +      from dvd_trans[OF p(2) qn1]
    1.10 +      have npp: "(n - 1) div p * p = n - 1" by simp
    1.11        with eq0 have "a^ (n - 1) = (n*s)^p"
    1.12          by (simp add: power_mult[symmetric])
    1.13        hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp