equal
deleted
inserted
replaced
65 |
65 |
66 |
66 |
67 subsection {* Basic Properties of the Gauss Sets *} |
67 subsection {* Basic Properties of the Gauss Sets *} |
68 |
68 |
69 lemma finite_A: "finite (A)" |
69 lemma finite_A: "finite (A)" |
70 apply (auto simp add: A_def) |
70 by (auto simp add: A_def) |
71 apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}") |
|
72 apply (auto simp add: bdd_int_set_l_finite finite_subset) |
|
73 done |
|
74 |
71 |
75 lemma finite_B: "finite (B)" |
72 lemma finite_B: "finite (B)" |
76 by (auto simp add: B_def finite_A) |
73 by (auto simp add: B_def finite_A) |
77 |
74 |
78 lemma finite_C: "finite (C)" |
75 lemma finite_C: "finite (C)" |