equal
deleted
inserted
replaced
10 *) |
10 *) |
11 |
11 |
12 section \<open>Set intervals\<close> |
12 section \<open>Set intervals\<close> |
13 |
13 |
14 theory Set_Interval |
14 theory Set_Interval |
15 imports Divides |
15 imports Parity |
16 begin |
16 begin |
17 |
17 |
18 (* Belongs in Finite_Set but 2 is not available there *) |
18 (* Belongs in Finite_Set but 2 is not available there *) |
19 lemma card_2_iff: "card S = 2 \<longleftrightarrow> (\<exists>x y. S = {x,y} \<and> x \<noteq> y)" |
19 lemma card_2_iff: "card S = 2 \<longleftrightarrow> (\<exists>x y. S = {x,y} \<and> x \<noteq> y)" |
20 by (auto simp: card_Suc_eq numeral_eq_Suc) |
20 by (auto simp: card_Suc_eq numeral_eq_Suc) |