[isabelle] Proving cardinality



Hi,

I'm trying to prove the cardinality of the set {1,2} being greater
than 1, but I seem to be able to only prove that the cardinality is
greater than 0:

axiomatization
S :: "nat set" where
ax1 : "S = {1,2}"

lemma "card S > 0"
using ax1
by (metis card_eq_0_iff finite.emptyI finite.insertI gr0I insert_not_empty)

Now I'm trying to prove:

lemma "card S > 1"
sledgehammer

but sledgehammer can't seem to find a proof. Could someone please help?

Thanks a lot for your time.

John





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.