proposition: Theorem Union_associative : forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
proof: Proof. auto 9 with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset