equal
deleted
inserted
replaced
109 assume c: "x \<le> (int p - 1) div 2" |
109 assume c: "x \<le> (int p - 1) div 2" |
110 assume d: "0 < y" |
110 assume d: "0 < y" |
111 assume e: "y \<le> (int p - 1) div 2" |
111 assume e: "y \<le> (int p - 1) div 2" |
112 from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y] |
112 from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y] |
113 have "[x = y](mod p)" |
113 have "[x = y](mod p)" |
114 by (metis comm_monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int |
114 by (metis monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int |
115 cong_mult_self_int gcd_int.commute prime_imp_coprime_int) |
115 cong_mult_self_int gcd_int.commute prime_imp_coprime_int) |
116 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
116 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
117 order_le_less_trans [of x "(int p - 1) div 2" p] |
117 order_le_less_trans [of x "(int p - 1) div 2" p] |
118 order_le_less_trans [of y "(int p - 1) div 2" p] |
118 order_le_less_trans [of y "(int p - 1) div 2" p] |
119 have "x = y" |
119 have "x = y" |