Proving Union of Ensemble is not Empty_set

Question

Working with the Ensembles library, I'd like to show that the union of an Ensemble with a singleton is not Empty_set.

Lemma aze: Singleton nat 1 <> Empty_set nat.

However, I have no idea how to prove that. I'd be happy to say what I tried, but except playing with auto, intro and simpl, I'm stuck.

Answer 1

1. Assume H1 : Singleton nat 1 = Empty_set nat (by intro H1). You now have to prove False.
2. Assert (= prove) H2 : Empty_set nat -> False.
3. Rewrite to H2 : Singleton nat 1 -> False via H1.
4. Assert H3 : Singleton nat 1.
5. H2 H3 : False.