equal
deleted
inserted
replaced
177 qed |
177 qed |
178 |
178 |
179 lemma int_card_bdd_int_set_l_l: "0 < n ==> |
179 lemma int_card_bdd_int_set_l_l: "0 < n ==> |
180 int(card {x. 0 < x & x < n}) = n - 1" |
180 int(card {x. 0 < x & x < n}) = n - 1" |
181 apply (auto simp add: card_bdd_int_set_l_l) |
181 apply (auto simp add: card_bdd_int_set_l_l) |
182 apply (subgoal_tac "Suc 0 \<le> nat n") |
|
183 apply (auto simp add: zdiff_int [symmetric]) |
|
184 apply (subgoal_tac "0 < nat n", arith) |
|
185 apply (simp add: zero_less_nat_eq) |
|
186 done |
182 done |
187 |
183 |
188 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> |
184 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> |
189 int(card {x. 0 < x & x \<le> n}) = n" |
185 int(card {x. 0 < x & x \<le> n}) = n" |
190 by (auto simp add: card_bdd_int_set_l_le) |
186 by (auto simp add: card_bdd_int_set_l_le) |