Subset.v

(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Martin, Mayero

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(** Operations on subsets (definitions and properties).

  Subsets of the type U are represented by their belonging function,
  of type U -> Prop.

  Most of the properties are tautologies that can be found on Wikipedia:
  https://en.wikipedia.org/wiki/List_of_set_identities_and_relations *)

From Coq Require Import Classical.
From Coq Require Import PropExtensionality FunctionalExtensionality.


Section Base_Def1.

Context {U : Type}. (* Universe. *)

(** Nullary constructors of subsets. *)

Definition emptyset : U -> Prop := fun _ => False.
Definition fullset : U -> Prop := fun _ => True.

(** Unary constructor of subsets. *)

Variable a : U. (* Element. *)

Definition singleton : U -> Prop := fun x => x = a.

(** Unary predicates on subsets. *)

Variable A : U -> Prop. (* Subset. *)

Definition empty : Prop := forall x, A x -> False.
Definition full : Prop := forall x, A x.

(** Unary operation on subsets. *)

Definition compl : U -> Prop := fun x => ~ A x.

(** Binary predicates on subsets. *)

Variable B : U -> Prop. (* Subset. *)

Definition incl : Prop := forall x, A x -> B x.
Definition same : Prop := forall x, A x <-> B x.

Definition disj : Prop :=forall x, A x -> B x -> False.

(** Binary operations on subsets. *)

Definition union : U -> Prop := fun x => A x \/ B x.
Definition inter : U -> Prop := fun x => A x /\ B x.

End Base_Def1.


Section Base_Def2.

Context {U : Type}. (* Universe. *)

(** Sesquary operation on subsets. *)

Variable A : U -> Prop. (* Subset. *)
Variable a : U. (* Element. *)

Definition add : U -> Prop := union A (singleton a).

(** More binary operation on subsets. *)

Variable B : U -> Prop. (* Subset. *)

Definition diff : U -> Prop := inter A (compl B).

(** Ternary predicate on subsets. *)

Variable C : U -> Prop. (* Subset. *)

Definition partition : Prop := A = union B C /\ disj B C.

End Base_Def2.


Section Base_Def3.

Context {U : Type}. (* Universe. *)

(** Binary constructor of subsets. *)

Variable a b : U. (* Elements. *)

Definition pair : U -> Prop := add (singleton a) b.

(** More binary operation on subsets. *)

Variable A B : U -> Prop. (* Subsets. *)

Definition sym_diff : U -> Prop := union (diff A B) (diff B A).

End Base_Def3.


Section Base_Def4.

Context {U1 U2 : Type}. (* Universes. *)

Variable A1 : U1 -> Prop. (* Subset. *)
Variable A2 : U2 -> Prop. (* Subset. *)

Definition prod : U1 * U2 -> Prop :=
  inter (fun x => A1 (fst x)) (fun x => A2 (snd x)).

Definition swap : forall {U : Type}, (U1 * U2 -> U) -> U2 * U1 -> U :=
  fun U f x => f (snd x, fst x).

End Base_Def4.


Ltac subset_unfold :=
  unfold partition, disj, same, incl, full, empty, (* Predicates. *)
      pair,
      swap, prod, sym_diff, diff, add, inter, union, compl, (* Operators. *)
      singleton, fullset, emptyset. (* Constructors. *)

Ltac subset_auto :=
  subset_unfold; try tauto; try easy.


Section Prop_Facts.

Context {U : Type}. (* Universe. *)

(** Extensionality of subsets. *)

Lemma subset_ext :
  forall (A B : U -> Prop),
    same A B -> A = B.
Proof.
intros.
apply functional_extensionality;
    intros x; now apply propositional_extensionality.
Qed.

Lemma subset_ext_equiv :
  forall (A B : U -> Prop),
    A = B <-> incl A B /\ incl B A.
Proof.
intros; split.
intros H; split; now rewrite H.
intros [H1 H2]; apply subset_ext; split; [apply H1 | apply H2].
Qed.

(** Facts about emptyset and fullset. *)

Lemma empty_emptyset :
  forall (A : U -> Prop),
    empty A <-> A = emptyset.
Proof.
intros; split; intros H.
intros; apply subset_ext; intros x; split; try easy; intros; now apply (H x).
now rewrite H.
Qed.

Lemma full_fullset :
  forall (A : U -> Prop),
    full A <-> A = fullset.
Proof.
intros; split; intros H.
now apply subset_ext.
now rewrite H.
Qed.

(** Facts about singleton. *)

Lemma singleton_in :
  forall a : U, singleton a a.
Proof.
subset_auto.
Qed.

Lemma singleton_out :
  forall a x : U, x <> a -> compl (singleton a) x.
Proof.
subset_auto.
Qed.

(** Facts about incl. *)

(** It is an order binary relation. *)

Lemma incl_refl :
  forall (A B : U -> Prop),
    same A B -> incl A B.
Proof.
intros A B H x; now rewrite (H x).
Qed.

Lemma incl_antisym :
  forall (A B : U -> Prop),
    incl A B -> incl B A -> A = B.
Proof.
intros; now rewrite subset_ext_equiv.
Qed.

Lemma incl_trans :
  forall (A B C : U -> Prop),
    incl A B -> incl B C -> incl A C.
Proof.
intros; intros x Hx; auto.
Qed.

Lemma full_not_empty :
  inhabited U <-> ~ incl (@fullset U) emptyset.
Proof.
subset_unfold; split.
intros [x]; auto.
intros H; apply exists_inhabited with (fun x => ~ (True -> False)).
now apply not_all_ex_not in H.
Qed.

Lemma incl_empty :
  forall (A : U -> Prop),
    incl A emptyset -> A = emptyset.
Proof.
intros A H; apply subset_ext; split; [apply H | easy].
Qed.

Lemma full_incl :
  forall (A : U -> Prop),
    incl fullset A -> A = fullset.
Proof.
intros A H; apply subset_ext; split; [easy | apply H].
Qed.

(** Facts about same. *)

(** It is an equivalence binary relation. *)

(* Useless?
Lemma same_refl :
  forall (A : U -> Prop),
    same A A.
Proof.
easy.
Qed.*)

(* This one is used! *)
Lemma same_sym :
  forall (A B : U -> Prop),
    same A B -> same B A.
Proof.
easy.
Qed.

Lemma same_trans :
  forall (A B C : U -> Prop),
    same A B -> same B C -> same A C.
Proof.
intros A B C H1 H2 x; now rewrite (H1 x).
Qed.

(** Facts about disj. *)

Lemma disj_equiv_def :
  forall (A B : U -> Prop),
    disj A B <-> inter A B = emptyset.
Proof.
intros; rewrite <- empty_emptyset; subset_unfold; split;
    intros H x; intros; now apply (H x).
Qed.

Lemma disj_irrefl :
  forall (A : U -> Prop),
    disj A A <-> A = emptyset.
Proof.
intros; rewrite <- empty_emptyset; split; intros H x Hx; now apply (H x).
Qed.

Lemma disj_sym :
  forall (A B : U -> Prop),
    disj A B <-> disj B A.
Proof.
intros; split; intros H x Hx1 Hx2; now apply (H x).
Qed.

Lemma disj_full_l :
  forall (A : U -> Prop),
    disj fullset A -> A = emptyset.
Proof.
intros A H; apply empty_emptyset; intros x Hx; now apply (H x).
Qed.

Lemma disj_full_r :
  forall (A : U -> Prop),
    disj A fullset -> A = emptyset.
Proof.
intros A; rewrite disj_sym; apply disj_full_l.
Qed.

Lemma disj_monot_l :
  forall (A B C : U -> Prop),
    incl A B ->
    disj B C -> disj A C.
Proof.
intros A B C H1 H2 x Hx1 Hx2; apply (H2 x); auto.
Qed.

Lemma disj_monot_r :
  forall (A B C : U -> Prop),
    incl A B ->
    disj C B -> disj C A.
Proof.
intros A B C H1 H2 x Hx1 Hx2; apply (H2 x); auto.
Qed.

Lemma incl_disj :
  forall (A B : U -> Prop),
    incl A B ->
    disj A B <-> A = emptyset.
Proof.
intros; split; intros H2.
apply empty_emptyset; intros x Hx; apply (H2 x); auto.
now rewrite H2.
Qed.

End Prop_Facts.


Section Compl_Facts.

(** Facts about complement. *)

Context {U : Type}. (* Universe. *)

Lemma compl_empty :
  compl (@emptyset U) = fullset.
Proof.
now apply subset_ext.
Qed.

Lemma compl_full :
  compl (@fullset U) = emptyset.
Proof.
apply subset_ext; subset_auto.
Qed.

Lemma compl_invol :
  forall (A : U -> Prop),
    compl (compl A) = A.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma incl_compl :
  forall (A B : U -> Prop),
    incl A B -> incl (compl B) (compl A).
Proof.
subset_auto; intros; intuition.
Qed.

Lemma incl_compl_equiv :
  forall (A B : U -> Prop),
    incl (compl B) (compl A) <-> incl A B.
Proof.
intros; split.
rewrite <- (compl_invol A) at 2; rewrite <- (compl_invol B) at 2.
apply incl_compl.
apply incl_compl.
Qed.

Lemma same_compl :
  forall (A B : U -> Prop),
    same A B -> same (compl A) (compl B).
Proof.
subset_unfold; intros; now apply not_iff_compat.
Qed.

Lemma same_compl_equiv :
  forall (A B : U -> Prop),
    same (compl A) (compl B) <-> same A B.
Proof.
intros; split.
rewrite <- (compl_invol A) at 2; rewrite <- (compl_invol B) at 2.
apply same_compl.
apply same_compl.
Qed.

Lemma compl_reg :
  forall (A B : U -> Prop),
    same (compl A) (compl B) -> A = B.
Proof.
intros; now apply subset_ext, same_compl_equiv.
Qed.

Lemma compl_ext :
  forall (A B : U -> Prop),
    compl A = compl B -> A = B.
Proof.
intros A B H; apply compl_reg; now rewrite H.
Qed.

Lemma disj_incl_compl_r :
  forall (A B : U -> Prop),
    disj A B <-> incl A (compl B).
Proof.
subset_auto.
Qed.

Lemma disj_incl_compl_l :
  forall (A B : U -> Prop),
    disj A B <-> incl B (compl A).
Proof.
intros A B; rewrite disj_sym; apply disj_incl_compl_r.
Qed.

End Compl_Facts.


Section Union_Facts.

(** Facts about union. *)

Context {U : Type}. (* Universe. *)

Lemma union_assoc :
  forall (A B C : U -> Prop),
    union (union A B) C = union A (union B C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma union_comm :
  forall (A B : U -> Prop),
    union A B = union B A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma union_idem :
  forall (A : U -> Prop),
    union A A = A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma union_empty_l :
  forall (A : U -> Prop),
    union emptyset A = A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma union_empty_r :
  forall (A : U -> Prop),
    union A emptyset = A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma empty_union :
  forall (A B : U -> Prop),
    union A B = emptyset <-> A = emptyset /\ B = emptyset.
Proof.
intros; do 3 rewrite <- empty_emptyset; split.
intros H; split; intros x Hx; apply (H x); [now left | now right].
intros [H1 H2] x [Hx | Hx]; [now apply (H1 x) | now apply (H2 x)].
Qed.

Lemma union_full_l :
  forall (A : U -> Prop),
    union fullset A = fullset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma union_full_r :
  forall (A : U -> Prop),
    union A fullset = fullset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma union_ub_l :
  forall (A B : U -> Prop),
    incl A (union A B).
Proof.
subset_auto.
Qed.

Lemma union_ub_r :
  forall (A B : U -> Prop),
    incl B (union A B).
Proof.
subset_auto.
Qed.

Lemma union_lub :
  forall (A B C : U -> Prop),
    incl A C -> incl B C ->
    incl (union A B) C.
Proof.
intros; intros x [H3 | H3]; auto.
Qed.

Lemma incl_union :
  forall (A B C : U -> Prop),
    incl (union A B) C -> incl A C /\ incl B C.
Proof.
intros A B C H; split; intros x Hx; apply (H x); [now left | now right].
Qed.

Lemma union_left :
  forall (A B : U -> Prop),
    incl A B <-> union B A = B.
Proof.
intros; split.
(* *)
intros; rewrite subset_ext_equiv; split; intros x.
intros [Hx | Hx]; auto.
intros Hx; now left.
(* *)
intros H x Hx; rewrite <- H; now right.
Qed.

Lemma union_right :
  forall (A B : U -> Prop),
    incl A B <-> union A B = B.
Proof.
intros A B; rewrite union_comm; apply union_left.
Qed.

Lemma union_monot_l :
  forall (A B C : U -> Prop),
    incl A B -> incl (union C A) (union C B).
Proof.
intros A B C H x [Hx | Hx]; [now left | right; now apply H].
Qed.

Lemma union_monot_r :
  forall (A B C : U -> Prop),
    incl A B -> incl (union A C) (union B C).
Proof.
intros; rewrite (union_comm A), (union_comm B); now apply union_monot_l.
Qed.

Lemma disj_union_l :
  forall (A B C : U -> Prop),
    disj (union A B) C <-> disj A C /\ disj B C.
Proof.
intros; split.
intros H; split; intros x Hx1 Hx2; apply (H x); try easy; [now left | now right].
intros [H1 H2] x [Hx1 | Hx1] Hx2; [now apply (H1 x) | now apply (H2 x)].
Qed.

Lemma disj_union_r :
  forall (A B C : U -> Prop),
    disj A (union B C) <-> disj A B /\ disj A C.
Proof.
intros A B C; now rewrite disj_sym, disj_union_l, (disj_sym B), (disj_sym C).
Qed.

Lemma union_compl_l :
  forall (A : U -> Prop),
    union (compl A) A = fullset.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma union_compl_r :
  forall (A : U -> Prop),
    union A (compl A) = fullset.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

End Union_Facts.


Section Inter_Facts.

(** Facts about intersection. *)

Context {U : Type}. (* Universe. *)

Lemma inter_assoc :
  forall (A B C : U -> Prop),
    inter (inter A B) C = inter A (inter B C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma inter_comm :
  forall (A B : U -> Prop),
    inter A B = inter B A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma inter_idem :
  forall (A : U -> Prop),
    inter A A = A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma inter_full_l :
  forall (A : U -> Prop),
    inter fullset A = A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma inter_full_r :
  forall (A : U -> Prop),
    inter A fullset = A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma full_inter :
  forall (A B : U -> Prop),
    inter A B = fullset <-> A = fullset /\ B = fullset.
Proof.
intros; do 3 rewrite <- full_fullset; split.
intros H; split; intros x; now destruct (H x).
intros [H1 H2] x; split; [apply (H1 x) | apply (H2 x)].
Qed.

Lemma inter_empty_l :
  forall (A : U -> Prop),
    inter emptyset A = emptyset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma inter_empty_r :
  forall (A : U -> Prop),
    inter A emptyset = emptyset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma inter_lb_l :
  forall (A B : U -> Prop),
    incl (inter A B) A.
Proof.
subset_auto.
Qed.

Lemma inter_lb_r :
  forall (A B : U -> Prop),
    incl (inter A B) B.
Proof.
subset_auto.
Qed.

Lemma inter_glb :
  forall (A B C : U -> Prop),
    incl C A -> incl C B ->
    incl C (inter A B).
Proof.
intros; intros x Hx; split; auto.
Qed.

Lemma incl_inter :
  forall (A B C : U -> Prop),
    incl A (inter B C) -> incl A B /\ incl A C.
Proof.
intros A B C H; split; intros x Hx; now apply (H x).
Qed.

Lemma inter_left :
  forall (A B : U -> Prop),
    incl A B <-> inter A B = A.
Proof.
intros; split.
(* *)
rewrite subset_ext_equiv; split; intros x.
intros [Hx1 Hx2]; auto.
intros Hx; split; auto.
(* *)
intros H x Hx; rewrite <- H in Hx; now destruct Hx as [_ Hx].
Qed.

Lemma inter_right :
  forall (A B : U -> Prop),
    incl B A <-> inter A B = B.
Proof.
intros; rewrite inter_comm; apply inter_left.
Qed.

Lemma inter_monot_l :
  forall (A B C : U -> Prop),
    incl A B -> incl (inter C A) (inter C B).
Proof.
intros A B C H x [Hx1 Hx2]; split; [easy | now apply H].
Qed.

Lemma inter_monot_r :
  forall (A B C : U -> Prop),
    incl A B -> incl (inter A C) (inter B C).
Proof.
intros; rewrite (inter_comm A), (inter_comm B); now apply inter_monot_l.
Qed.

Lemma disj_inter_l :
  forall (A B C : U -> Prop),
    disj A B -> disj (inter C A) (inter C B).
Proof.
intros A B C H; rewrite disj_equiv_def in H; rewrite disj_equiv_def.
rewrite <- empty_emptyset in H; rewrite <- empty_emptyset.
intros x [[_ Hx1] [_ Hx2]]; now apply (H x).
Qed.

Lemma disj_inter_r :
  forall (A B C : U -> Prop),
    disj A B -> disj (inter A C) (inter B C).
Proof.
intros; rewrite (inter_comm A), (inter_comm B); now apply disj_inter_l.
Qed.

Lemma inter_compl_l :
  forall (A : U -> Prop),
    inter (compl A) A = emptyset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma inter_compl_r :
  forall (A : U -> Prop),
    inter A (compl A) = emptyset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

End Inter_Facts.


Section Union_Inter_Facts.

(** Facts about union and intersection. *)

Context {U : Type}. (* Universe. *)

Lemma incl_inter_union :
  forall (A B : U -> Prop),
    incl (inter A B) (union A B).
Proof.
intros; intros x [Hx _]; now left.
Qed.

Lemma disj_inter_union :
  forall (A B : U -> Prop),
    disj (inter A B) (union A B) <-> disj A B.
Proof.
intros; split; intros H x.
intros Hx1 Hx2; apply (H x); [easy | now left].
intros [Hx1 Hx2] _; now apply (H x).
Qed.

(** De Morgan's laws. *)

Lemma compl_union :
  forall (A B : U -> Prop),
    compl (union A B) = inter (compl A) (compl B).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma compl_inter :
  forall (A B : U -> Prop),
    compl (inter A B) = union (compl A) (compl B).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

(** Distributivity. *)

Lemma distrib_union_union_l :
  forall (A B C : U -> Prop),
    union A (union B C) = union (union A B) (union A C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_union_union_r :
  forall (A B C : U -> Prop),
    union (union A B) C = union (union A C) (union B C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_union_inter_l :
  forall (A B C : U -> Prop),
    union A (inter B C) = inter (union A B) (union A C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_union_inter_r :
  forall (A B C : U -> Prop),
    union (inter A B) C = inter (union A C) (union B C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_union_inter :
  forall (A B C D : U -> Prop),
    union (inter A B) (inter C D) =
    inter (inter (union A C) (union B C)) (inter (union A D) (union B D)).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_inter_union_l :
  forall (A B C : U -> Prop),
    inter A (union B C) = union (inter A B) (inter A C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_inter_union_r :
  forall (A B C : U -> Prop),
    inter (union A B) C = union (inter A C) (inter B C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_inter_union :
  forall (A B C D : U -> Prop),
    inter (union A B) (union C D) =
    union (union (inter A C) (inter B C)) (union (inter A D) (inter B D)).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_inter_inter_l :
  forall (A B C : U -> Prop),
    inter A (inter B C) = inter (inter A B) (inter A C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma distrib_inter_inter_r :
  forall (A B C : U -> Prop),
    inter (inter A B) C = inter (inter A C) (inter B C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma disj_compl_l :
  forall (A B : U -> Prop),
    disj (compl A) B -> ~ empty B -> ~ disj A B.
Proof.
intros A B H1 H2 H3; rewrite disj_equiv_def in H1, H3.
contradict H2; apply empty_emptyset.
rewrite <- (inter_full_l B).
rewrite <- (union_compl_l A), distrib_inter_union_r, H1, H3.
now apply empty_union.
Qed.

Lemma disj_compl_r :
  forall (A B : U -> Prop),
    disj A (compl B) -> ~ empty A -> ~ disj A B.
Proof.
intros A B H1 H2.
rewrite disj_sym in H1; rewrite disj_sym.
now apply disj_compl_l.
Qed.

End Union_Inter_Facts.


Section Add_Facts.

(** Facts about addition of one element. *)

Context {U : Type}. (* Universe. *)

Lemma add_incl :
  forall A (a : U), incl A (add A a).
Proof.
intros; apply union_ub_l.
Qed.

Lemma add_in :
  forall A (a : U), add A a a.
Proof.
intros; apply union_ub_r, singleton_in.
Qed.

End Add_Facts.


Section Diff_Facts.

(** Facts about set difference. *)

Context {U : Type}. (* Universe. *)

Lemma diff_equiv_def_inter :
  forall (A B : U -> Prop),
    diff A B = inter A (compl B).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_equiv_def_union :
  forall (A B : U -> Prop),
    diff A B = compl (union (compl A) B).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma compl_equiv_def_diff :
  forall (A : U -> Prop),
    compl A = diff fullset A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma inter_equiv_def_diff :
  forall (A B : U -> Prop),
    inter A B = diff A (diff A B).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma union_equiv_def_diff :
  forall (A B : U -> Prop),
    union A B = compl (diff (compl A) B).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff_lb_l :
  forall (A B : U -> Prop),
    incl (diff A B) A.
Proof.
intros; apply inter_lb_l.
Qed.

Lemma diff_lb_r :
  forall (A B : U -> Prop),
    incl (diff A B) (compl B).
Proof.
intros; apply inter_lb_r.
Qed.

Lemma partition_diff_l :
  forall (A B : U -> Prop),
    partition (union A B) (diff A B) B.
Proof.
intros; split.
apply subset_ext; intros x; subset_auto.
subset_auto.
Qed.

Lemma partition_diff_r :
  forall (A B : U -> Prop),
    partition (union A B) A (diff B A).
Proof.
intros; split.
apply subset_ext; intros x; subset_auto.
subset_auto.
Qed.

Lemma diff_monot_l :
  forall (A B C : U -> Prop),
    incl B C -> incl (diff A C) (diff A B).
Proof.
intros A B C H x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
Qed.

Lemma diff_monot_r :
  forall (A B C : U -> Prop),
    incl A B -> incl (diff A C) (diff B C).
Proof.
intros A B C H x [Hx1 Hx2]; split; [now apply H | easy].
Qed.

Lemma disj_diff :
  forall (A B : U -> Prop),
    disj A B <-> diff A B = A.
Proof.
intros; rewrite subset_ext_equiv; split.