equal
deleted
inserted
replaced
1543 apply(auto elim!: card_eq_SucD) |
1543 apply(auto elim!: card_eq_SucD) |
1544 apply(subst card.insert) |
1544 apply(subst card.insert) |
1545 apply(auto simp add: intro:ccontr) |
1545 apply(auto simp add: intro:ccontr) |
1546 done |
1546 done |
1547 |
1547 |
|
1548 lemma card_1_singletonE: |
|
1549 assumes "card A = 1" obtains x where "A = {x}" |
|
1550 using assms by (auto simp: card_Suc_eq) |
|
1551 |
1548 lemma card_le_Suc_iff: "finite A \<Longrightarrow> |
1552 lemma card_le_Suc_iff: "finite A \<Longrightarrow> |
1549 Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)" |
1553 Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)" |
1550 by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff |
1554 by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff |
1551 dest: subset_singletonD split: nat.splits if_splits) |
1555 dest: subset_singletonD split: nat.splits if_splits) |
1552 |
1556 |