proposition: Lemma Setminus_Union_r: forall A s1 s2 s3, Setminus A s1 (Union A s2 s3) = Setminus A (Setminus A s1 s2) s3.
proof: Proof. intros. apply Extensionality_Ensembles. split. * intros x H. inversion H. constructor. -- intuition. -- contradict H1. intuition. * intros x H. inversion H. inversion H0. constructor; intuition. inversion H4; intuition. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset