equal
deleted
inserted
replaced
206 next |
206 next |
207 case (Un a t) |
207 case (Un a t) |
208 let ?e = evnodd |
208 let ?e = evnodd |
209 note hyp = \<open>card (?e t 0) = card (?e t 1)\<close> |
209 note hyp = \<open>card (?e t 0) = card (?e t 1)\<close> |
210 and at = \<open>a \<subseteq> - t\<close> |
210 and at = \<open>a \<subseteq> - t\<close> |
211 have card_suc: "b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))" for b :: nat |
211 have card_suc: "card (?e (a \<union> t) b) = Suc (card (?e t b))" if "b < 2" for b :: nat |
212 proof - |
212 proof - |
213 assume "b < 2" |
|
214 have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un) |
213 have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un) |
215 also obtain i j where e: "?e a b = {(i, j)}" |
214 also obtain i j where e: "?e a b = {(i, j)}" |
216 proof - |
215 proof - |
217 from \<open>a \<in> domino\<close> and \<open>b < 2\<close> |
216 from \<open>a \<in> domino\<close> and \<open>b < 2\<close> |
218 have "\<exists>i j. ?e a b = {(i, j)}" by (rule domino_singleton) |
217 have "\<exists>i j. ?e a b = {(i, j)}" by (rule domino_singleton) |