Library usingensembles

Require Import Classical_sets.
Require Import Ensembles.
Require Import Finite_sets.
Require Import Finite_sets_facts.
Require Import Integers.
Require Import Omega.
Require Import Arith.
Print Ensemble.

Print Empty_set.

Print Extensionality_Ensembles.
Print Same_set.
Print Singleton_is_finite.
Print Integers.
Variable U : Type.

Inductive myEmpty_set (U:Type) : Ensemble U :=.

Print card_empty.

Print Singleton.

Theorem empty_has_0 : cardinal U (Empty_set U) 0.

Theorem nempty_has_0 : cardinal nat (Empty_set nat) 0.

Print Empty_set.
Print myEmpty_set.

Theorem same_empty :
 Same_set U (Empty_set U) (myEmpty_set U).

Theorem empty_eq : (Empty_set U)=(myEmpty_set U).
Print empty_eq.

Theorem myempty_has_0 : cardinal U (myEmpty_set U) 0.

Print Couple.
Inductive unoydos : Ensemble nat :=
|unoydos_uno : In nat unoydos 1
|unoydos_dos : In nat unoydos 2
.

Theorem unoydos_as_singl :
unoydos=Union nat (Singleton nat 1) (Singleton nat 2).

Theorem singleton_has_one :
forall x:nat, cardinal nat (Singleton nat x) 1.

Theorem singleton_has_equals :
forall x y:nat, In nat (Singleton nat x) y -> x=y.

Theorem unoydos_has2 : cardinal nat unoydos 2.

Inductive range (a b:nat) : Ensemble nat :=
range_elems : forall n:nat, a<=n -> n<=b
 -> In nat (range a b) n.

Theorem range_elems_rec : forall a b n,
In nat (range a b) n -> (a<=n /\ n<=b).

Theorem range_in_integers : forall a b:nat,
 Included nat (range a b) Integers.

Theorem empty_range : forall a b:nat,
 b<a -> (range a b) = (Empty_set nat).

Theorem singleton_range : forall a:nat,
 (range a a)=(Singleton nat a).

Theorem split_range : forall a b:nat,
 a<b -> (range a b) =
  Union nat (range a (b-1)) (Singleton nat b).

Theorem nonempty_range : forall a b:nat,
 a<=b -> cardinal nat (range a b) (b-a+1).