Proving X ∪ Y ∪ Z ∩ X ∪ Y ∩ (X \ Z) = X ∪ Y in Coq

SetExample.coq

Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Powerset_facts.
Require Import Coq.Setoids.Setoid.

Section SetExample.

Variable U: Type.
Definition USet := Ensemble U.

Notation "X ∩ Y" := (Intersection U X Y) (at level 41).
Notation "X ∪ Y" := (Union U X Y) (at level 42).
Notation "X \ Y" := (Setminus U X Y) (at level 40).

Lemma Union_elimination: 
  forall (X Y: USet), X ∪ (X ∩ Y) = X.
Proof.
  intros.
  apply Union_absorbs.
  apply Intersection_decreases_l.
Qed.

Example ex1: forall (X Y Z: USet), 
  X ∪ Y ∪ Z ∩ X ∪ Y ∩ (X \ Z) = X ∪ Y.
Proof.
  intros.
  rewrite (Union_commutative U X Y).
  rewrite (Union_associative U Y X (Z ∩ X)).
  rewrite (Intersection_commutative U Z X).
  rewrite Union_elimination.
  rewrite (Union_commutative U Y X).
  rewrite Union_associative.
  rewrite Union_elimination.
  reflexivity.
Qed.

End SetExample.