equal
deleted
inserted
replaced
194 moreover from x have "x mod int p \<noteq> 0" |
194 moreover from x have "x mod int p \<noteq> 0" |
195 using B_ncong_p cong_int_def by simp |
195 using B_ncong_p cong_int_def by simp |
196 moreover have "int y = 0 \<or> 0 < int y" for y |
196 moreover have "int y = 0 \<or> 0 < int y" for y |
197 by linarith |
197 by linarith |
198 ultimately show "0 < x mod int p" |
198 ultimately show "0 < x mod int p" |
199 by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int) |
199 using B_greater_zero [of x] |
|
200 by (auto simp add: mod_int_pos_iff intro: neq_le_trans) |
200 qed |
201 qed |
201 |
202 |
202 lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}" |
203 lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}" |
203 apply (auto simp add: F_def E_def C_def) |
204 apply (auto simp add: F_def E_def C_def) |
204 apply (metis p_ge_2 Divides.pos_mod_bound nat_int zless_nat_conj) |
205 apply (metis p_ge_2 Divides.pos_mod_bound nat_int zless_nat_conj) |