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