--- a/src/HOL/Set_Interval.thy Sat Feb 15 21:15:03 2020 +0100
+++ b/src/HOL/Set_Interval.thy Sun Feb 16 18:01:03 2020 +0100
@@ -15,6 +15,13 @@
imports Divides
begin
+(* Belongs in Finite_Set but 2 is not available there *)
+lemma card_2_iff: "card S = 2 \<longleftrightarrow> (\<exists>x y. S = {x,y} \<and> x \<noteq> y)"
+by (auto simp: card_Suc_eq numeral_eq_Suc)
+
+lemma card_2_iff': "card S = 2 \<longleftrightarrow> (\<exists>x\<in>S. \<exists>y\<in>S. x \<noteq> y \<and> (\<forall>z\<in>S. z = x \<or> z = y))"
+by (auto simp: card_Suc_eq numeral_eq_Suc)
+
context ord
begin