changeset 66801 | f3fda9777f9a |
parent 65416 | f707dbcf11e3 |
child 66837 | 6ba663ff2b1c |
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun Oct 08 22:28:19 2017 +0200 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun Oct 08 22:28:20 2017 +0200 @@ -381,7 +381,7 @@ from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x" by force from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x" - by (auto simp: semiring_numeral_div_class.div_less) + by (auto simp: div_pos_pos_trivial) with * show "f_3 (g_3 x) = x" by (simp add: f_3_def g_3_def) qed