(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

Require Import Ensembles.
Require Import Relations_1.
Require Import Partial_Order.
Require Import Cpo.
Require Import algpodefs.
Require Import Powerset.
Require Import Constructive_sets.
Require Import Finite_sets.
Require Import lpo.
Require Import lpo1.
Section Advanced_lemmas.
Variable U : Type.
Variable D : PO U.
Hint Resolve Lub_definition Upper_Bound_Couple_intro.

Lemma Lub_monotonic :
 forall A B : Ensemble U,
 Included U A B ->
 Included U B (Carrier_of U D) ->
 forall a b : U, Lub U D A a -> Lub U D B b -> Rel_of U D a b.
(* Goal: forall (A B : Ensemble U) (_ : Included U A B) (_ : Included U B (Carrier_of U D)) (a b : U) (_ : Lub U D A a) (_ : Lub U D B b), Rel_of U D a b *)
intros A B H' H'0 a b H'1 H'2; try assumption.
(* Goal: Rel_of U D a b *)
elim H'1; auto with sets.
(* Goal: forall (_ : Upper_Bound U D A a) (_ : forall (y : U) (_ : Upper_Bound U D A y), Rel_of U D a y), Rel_of U D a b *)
intros H'3 H'4; apply H'4.
(* Goal: Upper_Bound U D A b *)
apply Upper_downward_stable with (B := B); auto with sets.
(* Goal: Rel_of U D bot x *)
(* Goal: forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) (Approximants U D x)), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
elim H'2; auto with sets.
Qed.

Lemma Compatible_lubs :
 forall A B C : Ensemble U,
 Included U A C ->
 Included U B C ->
 Included U C (Carrier_of U D) ->
 forall a b c : U,
 Lub U D A a -> Lub U D B b -> Lub U D C c -> Compatible U D a b.
(* Goal: forall (A B C : Ensemble U) (_ : Included U A C) (_ : Included U B C) (_ : Included U C (Carrier_of U D)) (a b c : U) (_ : Lub U D A a) (_ : Lub U D B b) (_ : Lub U D C c), Compatible U D a b *)
intros A B C H' H'0 H'1 a b c H'2 H'3 H'4; red in |- *; simpl in |- *.
(* Goal: forall (_ : In U (Carrier_of U D) a) (_ : In U (Carrier_of U D) b), @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U a b) z)) *)
intros H'5 H'6; exists c; split.
(* Goal: In U (Carrier_of U D) c *)
(* Goal: Rel_of U D a c *)
(* Goal: Rel_of U D b c *)
apply Lub_is_in_Carrier with (X := C); auto with sets.
(* Goal: Upper_Bound U D (Couple U a b) c *)
apply Upper_Bound_Couple_intro; auto with sets.
(* Goal: In U (Carrier_of U D) c *)
(* Goal: Rel_of U D a c *)
(* Goal: Rel_of U D b c *)
apply Lub_is_in_Carrier with (X := C); auto with sets.
(* Goal: Rel_of U D a c *)
(* Goal: Rel_of U D b c *)
apply Lub_monotonic with (A := A) (B := C); auto with sets.
(* Goal: Rel_of U D b c *)
apply Lub_monotonic with (A := B) (B := C); auto with sets.
Qed.

Lemma LUaux :
 forall A B : Ensemble U,
 Included U (Union U A B) (Carrier_of U D) ->
 forall a b bsup : U,
 Lub U D A a ->
 Lub U D B b -> Lub U D (Union U A B) bsup -> Lub U D (Couple U a b) bsup.
(* Goal: forall (c : U) (_ : Compact U D c) (_ : Rel_of U D c x), In U (Approximants U D y) c *)
generalize Rel_of_transitive; intro RoT; red in RoT.
(* Goal: forall (A B : Ensemble U) (_ : Included U (Union U A B) (Carrier_of U D)) (a b bsup : U) (_ : Lub U D A a) (_ : Lub U D B b) (_ : Lub U D (Couple U a b) bsup), Lub U D (Union U A B) bsup *)
intros A B H' a b bsup H'0 H'1 H'2; try assumption.
(* Goal: Lub U D (Union U A B) bsup *)
elim H'0; elim H'1; elim H'2.
(* Goal: forall (_ : Upper_Bound U D (Couple U a b) bsup) (_ : forall (y : U) (_ : Upper_Bound U D (Couple U a b) y), Rel_of U D bsup y) (_ : Upper_Bound U D B b) (_ : forall (y : U) (_ : Upper_Bound U D B y), Rel_of U D b y) (_ : Upper_Bound U D A a) (_ : forall (y : U) (_ : Upper_Bound U D A y), Rel_of U D a y), Lub U D (Union U A B) bsup *)
intros H'3 H'4 H'5 H'6 H'7 H'8; try assumption.
(* Goal: Lub U D (Couple U a b) bsup *)
elim H'3; elim H'5; elim H'7.
(* Goal: forall (_ : In U (Carrier_of U D) a) (_ : forall (y : U) (_ : In U A y), Rel_of U D y a) (_ : In U (Carrier_of U D) b) (_ : forall (y : U) (_ : In U B y), Rel_of U D y b) (_ : In U (Carrier_of U D) bsup) (_ : forall (y : U) (_ : In U (Union U A B) y), Rel_of U D y bsup), Lub U D (Couple U a b) bsup *)
intros H'9 H'10 H'11 H'12 H'13 H'14; try assumption.
(* Goal: Lub U D (Couple U a b) bsup *)
apply Lub_definition; auto 8 with sets.
(* Goal: forall (y : U) (_ : Upper_Bound U D (Couple U a b) y), Rel_of U D bsup y *)
intros y H'15; apply H'4.
(* Goal: Upper_Bound U D (Approximants U D y) y *)
apply Upper_Bound_definition; auto with sets.
(* Goal: In U (Carrier_of U D) y *)
(* Goal: forall (y0 : U) (_ : In U (Union U A B) y0), Rel_of U D y0 y *)
elim H'15; auto with sets.
elim (Upper_Bound_Couple_inv U D a b y);
 [ intros H'22 H'23; elim H'23; intros H'24 H'25; try exact H'24; clear H'23
 | idtac ]; auto with sets.
(* Goal: forall (y0 : U) (_ : In U (Union U A B) y0), Rel_of U D y0 y *)
intros y0 H'16; elim H'16.
(* Goal: forall (x : U) (_ : In U A x), Rel_of U D x y *)
(* Goal: forall (x : U) (_ : In U B x), Rel_of U D x y *)
intros x H'17; apply RoT with (y := a); auto with sets.
(* Goal: forall (x : U) (_ : In U B x), Rel_of U D x y *)
intros x H'17; apply RoT with (y := b); auto with sets.
Qed.

Lemma LUaux2 :
 forall A B : Ensemble U,
 Included U (Union U A B) (Carrier_of U D) ->
 forall a b bsup : U,
 Lub U D A a ->
 Lub U D B b -> Lub U D (Couple U a b) bsup -> Lub U D (Union U A B) bsup.
(* Goal: forall (c : U) (_ : Compact U D c) (_ : Rel_of U D c x), In U (Approximants U D y) c *)
generalize Rel_of_transitive; intro RoT; red in RoT.
(* Goal: forall (A B : Ensemble U) (_ : Included U (Union U A B) (Carrier_of U D)) (a b bsup : U) (_ : Lub U D A a) (_ : Lub U D B b) (_ : Lub U D (Couple U a b) bsup), Lub U D (Union U A B) bsup *)
intros A B H' a b bsup H'0 H'1 H'2; try assumption.
(* Goal: Lub U D (Union U A B) bsup *)
elim H'0; elim H'1; elim H'2.
(* Goal: forall (_ : Upper_Bound U D (Couple U a b) bsup) (_ : forall (y : U) (_ : Upper_Bound U D (Couple U a b) y), Rel_of U D bsup y) (_ : Upper_Bound U D B b) (_ : forall (y : U) (_ : Upper_Bound U D B y), Rel_of U D b y) (_ : Upper_Bound U D A a) (_ : forall (y : U) (_ : Upper_Bound U D A y), Rel_of U D a y), Lub U D (Union U A B) bsup *)
intros H'3 H'4 H'5 H'6 H'7 H'8; try assumption.
(* Goal: Lub U D (Union U A B) bsup *)
elim H'5; elim H'7.
elim (Upper_Bound_Couple_inv U D a b bsup);
 [ intros H'15 H'16; elim H'16; intros H'17 H'18; try exact H'17; clear H'16
 | idtac ]; auto with sets.
(* Goal: forall (_ : In U (Carrier_of U D) a) (_ : forall (y : U) (_ : In U A y), Rel_of U D y a) (_ : In U (Carrier_of U D) b) (_ : forall (y : U) (_ : In U B y), Rel_of U D y b), Lub U D (Union U A B) bsup *)
intros H'9 H'10 H'11 H'12; try assumption.
(* Goal: Lub U D (Empty_set U) bot *)
(* Goal: forall (A : Ensemble U) (_ : Finite U A) (_ : forall _ : Included U A (Approximants U D x), @ex U (fun bsup : U => and (Lub U D A bsup) (Approximant U D x bsup))) (x0 : U) (_ : not (In U A x0)) (_ : Included U (Add U A x0) (Approximants U D x)), @ex U (fun bsup : U => and (Lub U D (Add U A x0) bsup) (Approximant U D x bsup)) *)
apply Lub_definition; auto with sets.
(* Goal: Upper_Bound U D (Approximants U D y) y *)
apply Upper_Bound_definition; auto with sets.
(* Goal: forall (y : U) (_ : In U (Union U A B) y), Rel_of U D y bsup *)
(* Goal: forall (y : U) (_ : Upper_Bound U D (Union U A B) y), Rel_of U D bsup y *)
intros y H'13; elim H'13.
(* Goal: forall (x : U) (_ : In U A x), Rel_of U D x bsup *)
(* Goal: forall (x : U) (_ : In U B x), Rel_of U D x bsup *)
(* Goal: forall (y : U) (_ : Upper_Bound U D (Union U A B) y), Rel_of U D bsup y *)
intros x H'30; apply RoT with (y := a); auto with sets.
(* Goal: forall (x : U) (_ : In U B x), Rel_of U D x bsup *)
(* Goal: forall (y : U) (_ : Upper_Bound U D (Union U A B) y), Rel_of U D bsup y *)
intros x H'30; apply RoT with (y := b); auto with sets.
(* Goal: forall (y : U) (_ : Upper_Bound U D (Union U A B) y), Rel_of U D bsup y *)
intros y H'13; try assumption.
(* Goal: Rel_of U D bsup y *)
apply H'4.
(* Goal: Upper_Bound U D (Couple U a b) y *)
elim H'13; auto 7 with sets.
Qed.

Theorem Lub_of_Union :
 Conditionally_complete U D ->
 forall A B : Ensemble U,
 Included U (Union U A B) (Carrier_of U D) ->
 forall x : U,
 In U (Carrier_of U D) x ->
 Upper_Bound U D (Union U A B) x ->
 forall a b : U,
 Lub U D A a ->
 Lub U D B b ->
 exists bsup : U, Lub U D (Union U A B) bsup /\ Lub U D (Couple U a b) bsup.
intro H'; elim H'.
intros H'0 A B H'1 x H'2 H'3 a b H'4 H'5; try assumption.
elim (H'0 (Union U A B)); [ intros bsup E; try exact E | idtac | idtac ];
 auto with sets.
2: exists x; try assumption.
exists bsup; split; [ try assumption | idtac ].
apply LUaux with (A := A) (B := B); auto with sets.
Qed.

Theorem Lub_of_compacts_is_compact :
 Conditionally_complete U D ->
 forall x y z : U,
 Included U (Couple U x y) (Approximants U D z) ->
 In U (Carrier_of U D) z ->
 exists bsup : U, Lub U D (Couple U x y) bsup /\ Approximant U D z bsup.
Proof.
intros H' x y z H'0 K; red in H'0.
elim (H'0 x); auto with sets.
intros c H'1 H'2.
elim (H'0 y); auto with sets.
intros c' H'3 H'4.
(* Goal: Compact U D x *)
(* Goal: Conditionally_complete U D *)
elim H'.
intro H'5; elim (H'5 (Couple U c c')); auto with sets.
2: elim H'1; elim H'3; exists z; auto with sets.
intros bsup H'6; elim H'6.
intros H'7 H'8; exists bsup; split; auto with sets.
apply Defn_of_Approximant; auto with sets.
apply Definition_of_compact.
apply Lub_is_in_Carrier with (X := Couple U c c'); auto with sets.
intros X H'9 H'10.
elim H'1.
intros H'11 H'12; try assumption.
(* Goal: @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
elim H'3.
intros H'13 H'14; try assumption.
clear H'1 H'3.
elim H'10; intros bsup0 h; elim h; clear H'10 h.
intros H'1 H'3; try assumption.
(* Goal: forall (c : U) (_ : Compact U D c) (_ : Rel_of U D c x), In U (Approximants U D y) c *)
generalize Rel_of_transitive; intro RoT; red in RoT.
elim (H'14 X); auto with sets.
intros x0 H'10; elim H'10; intros H'15 H'17; try exact H'17; clear H'10.
elim (H'12 X); auto with sets.
intros x1 H'10; elim H'10; intros H'18 H'20; try exact H'20; clear H'10.
elim H'9.
intros H'10 H'21 H'22; elim (H'22 x0 x1); auto with sets.
intros y' H'23; elim H'23; intros H'24 H'26; try exact H'24; clear H'23.
exists y'; split; auto with sets.
apply H'8.
elim (Upper_Bound_Couple_inv U D x0 x1 y');
 [ intros H'29 H'30; elim H'30; intros H'31 H'32; clear H'30 | idtac ];
 auto with sets.
(* Goal: Upper_Bound U D (Couple U a b) c *)
apply Upper_Bound_Couple_intro; auto with sets.
apply RoT with (y := x1); auto with sets.
apply RoT with (y := x0); auto with sets.
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
red in |- *; simpl in |- *.
intros x2 H'23; elim H'23; auto with sets.
exists bsup0; split; auto with sets.
elim (Upper_Bound_Couple_inv U D c c' bsup);
 [ intros H'22 H'23; elim H'23; intros H'24 H'25; clear H'23 | idtac ];
 auto with sets.
apply RoT with (y := bsup); auto with sets.
exists bsup0; split; auto with sets.
elim (Upper_Bound_Couple_inv U D c c' bsup);
 [ intros H'20 H'21; elim H'21; intros H'22 H'23; clear H'21 | idtac ];
 auto with sets.
apply RoT with (y := bsup); auto with sets.
Qed.

Theorem approximants_closed_by_finite_lubs :
 Conditionally_complete U D ->
 forall (x : U) (C : Ensemble U),
 In U (Carrier_of U D) x ->
 Finite U C ->
 Included U C (Approximants U D x) ->
 exists bsup : U, Lub U D C bsup /\ Approximant U D x bsup.
(* Goal: forall (_ : Conditionally_complete U D) (x : U) (C : Ensemble U) (_ : In U (Carrier_of U D) x) (_ : Finite U C) (_ : Included U C (Approximants U D x)), @ex U (fun bsup : U => and (Lub U D C bsup) (Approximant U D x bsup)) *)
intros H' x C H H'0; elim H'0.
elim (Bottom_is_compact U D);
 [ intros bot E; elim E; intros H'4 H'5; elim H'4; clear E | idtac ];
 auto with sets.
(* Goal: forall (_ : In U (Carrier_of U D) bot) (_ : forall (y : U) (_ : In U (Carrier_of U D) y), Rel_of U D bot y) (_ : Included U (Empty_set U) (Approximants U D x)), @ex U (fun bsup : U => and (Lub U D (Empty_set U) bsup) (Approximant U D x bsup)) *)
(* Goal: forall (A : Ensemble U) (_ : Finite U A) (_ : forall _ : Included U A (Approximants U D x), @ex U (fun bsup : U => and (Lub U D A bsup) (Approximant U D x bsup))) (x0 : U) (_ : not (In U A x0)) (_ : Included U (Add U A x0) (Approximants U D x)), @ex U (fun bsup : U => and (Lub U D (Add U A x0) bsup) (Approximant U D x bsup)) *)
exists bot; split; auto with sets; auto with sets.
(* Goal: Lub U D (Empty_set U) bot *)
(* Goal: forall (A : Ensemble U) (_ : Finite U A) (_ : forall _ : Included U A (Approximants U D x), @ex U (fun bsup : U => and (Lub U D A bsup) (Approximant U D x bsup))) (x0 : U) (_ : not (In U A x0)) (_ : Included U (Add U A x0) (Approximants U D x)), @ex U (fun bsup : U => and (Lub U D (Add U A x0) bsup) (Approximant U D x bsup)) *)
apply Lub_definition; auto with sets.
(* Goal: Rel_of U D a b *)
intros y H'1; elim H'1; auto with sets.
(* Goal: forall (A : Ensemble U) (_ : Finite U A) (_ : forall _ : Included U A (Approximants U D x), @ex U (fun bsup : U => and (Lub U D A bsup) (Approximant U D x bsup))) (x0 : U) (_ : not (In U A x0)) (_ : Included U (Add U A x0) (Approximants U D x)), @ex U (fun bsup : U => and (Lub U D (Add U A x0) bsup) (Approximant U D x bsup)) *)
intros A H'1 H'2 x0 H'3.
(* Goal: forall _ : Included U (Add U A x0) (Approximants U D x), @ex U (fun bsup : U => and (Lub U D (Add U A x0) bsup) (Approximant U D x bsup)) *)
cut (forall x : U, Union U A (Singleton U x) = Add U A x); auto with sets.
(* Goal: forall (_ : forall x : U, @eq (Ensemble U) (Union U A (Singleton U x)) (Add U A x)) (_ : Included U (Add U A x0) (Approximants U D x)), @ex U (fun bsup : U => and (Lub U D (Add U A x0) bsup) (Approximant U D x bsup)) *)
intro H'4; rewrite <- (H'4 x0).
(* Goal: forall _ : Included U (Union U A (Singleton U x0)) (Approximants U D x), @ex U (fun bsup : U => and (Lub U D (Union U A (Singleton U x0)) bsup) (Approximant U D x bsup)) *)
clear H'4; intro H'4.
elim H'2; [ intros bsup E; elim E; intros H'6 H'7; clear E H'2 | clear H'2 ];
 auto with sets.
(* Goal: @ex U (fun bsup : U => and (Lub U D (Union U A (Singleton U x0)) bsup) (Approximant U D x bsup)) *)
red in H'4.
lapply Lub_of_Union;
 [ intro H'2; lapply (H'2 A (Singleton U x0));
    [ intro H'9; lapply (H'9 x);
       [ intro H'11; lapply H'11;
          [ intro H'12; elim (H'12 bsup x0);
             [ intros bsup0 E; elim E; intros H'17 H'18; try exact H'17;
                clear E H'11
             | clear H'11
             | clear H'11 ]
          | clear H'11 ]
       | idtac ]
    | idtac ]
 | idtac ]; auto with sets.
(* Goal: @ex U (fun bsup : U => and (Lub U D (Union U A (Singleton U x0)) bsup) (Approximant U D x bsup)) *)
(* Goal: Lub U D (Singleton U x0) x0 *)
(* Goal: Upper_Bound U D (Union U A (Singleton U x0)) x *)
(* Goal: Included U (Union U A (Singleton U x0)) (Carrier_of U D) *)
exists bsup0; split; [ assumption | auto with sets ].
lapply Lub_of_compacts_is_compact;
 [ intro H'5; elim (H'5 bsup x0 x);
    [ intros bsup1 E; elim E; intros H'15 H'16; try exact H'16; clear E
    | idtac
    | idtac ]
 | idtac ]; auto with sets.
lapply (Lub_is_unique U D);
 [ intro H'11; rewrite (H'11 (Couple U bsup x0) bsup0 bsup1) | idtac ];
 auto with sets.
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
red in |- *; simpl in |- *.
(* Goal: forall (x1 : U) (_ : In U (Couple U bsup x0) x1), In U (Approximants U D x) x1 *)
(* Goal: Lub U D (Singleton U x0) x0 *)
(* Goal: Upper_Bound U D (Union U A (Singleton U x0)) x *)
(* Goal: Included U (Union U A (Singleton U x0)) (Carrier_of U D) *)
intros x1 H'8; elim H'8; auto with sets.
(* Goal: In U (Approximants U D x) bsup *)
(* Goal: Lub U D (Singleton U x0) x0 *)
(* Goal: Upper_Bound U D (Union U A (Singleton U x0)) x *)
(* Goal: Included U (Union U A (Singleton U x0)) (Carrier_of U D) *)
elim H'7; auto with sets.
(* Goal: Lub U D (Singleton U x0) x0 *)
(* Goal: Upper_Bound U D (Union U A (Singleton U x0)) x *)
(* Goal: Included U (Union U A (Singleton U x0)) (Carrier_of U D) *)
apply Singleton_has_lub.
(* Goal: In U (Carrier_of U D) x0 *)
(* Goal: Upper_Bound U D (Union U A (Singleton U x0)) x *)
(* Goal: Included U (Union U A (Singleton U x0)) (Carrier_of U D) *)
lapply (H'4 x0); [ intro H'8; elim H'8 | idtac ]; auto with sets.
(* Goal: Upper_Bound U D (Approximants U D y) y *)
apply Upper_Bound_definition; auto with sets.
(* Goal: forall (y : U) (_ : In U (Union U A (Singleton U x0)) y), Rel_of U D y x *)
(* Goal: Included U (Union U A (Singleton U x0)) (Carrier_of U D) *)
intros y H'5; try assumption.
(* Goal: Rel_of U D y x *)
(* Goal: Included U (Union U A (Singleton U x0)) (Carrier_of U D) *)
lapply (H'4 y); [ intro H'10; elim H'10 | idtac ]; auto with sets.
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
red in |- *; simpl in |- *.
(* Goal: forall (x : U) (_ : In U (Union U A (Singleton U x0)) x), In U (Carrier_of U D) x *)
intros x1 H'5; try assumption.
(* Goal: In U (Carrier_of U D) x1 *)
lapply (H'4 x1); [ intro H'9; elim H'9 | idtac ]; auto with sets.
Qed.

Theorem Approximants_directed_set :
 Conditionally_complete U D ->
 forall x : U, In U (Carrier_of U D) x -> Directed U D (Approximants U D x).
Proof.
(* Goal: forall (_ : Conditionally_complete U D) (x : U) (_ : In U (Carrier_of U D) x), Directed U D (Approximants U D x) *)
intros H' x H'0; constructor 1; auto with sets.
(* Goal: Rel_of U D a b *)
red in |- *; simpl in |- *; intros x0 H'1; elim H'1; auto with sets.
(* Goal: Inhabited U (Approximants U D x) *)
(* Goal: forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) (Approximants U D x)), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
elim (Bottom_is_compact U D); auto with sets.
(* Goal: forall (x0 : U) (_ : and (Bottom U D x0) (Compact U D x0)), Inhabited U (Approximants U D x) *)
(* Goal: forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) (Approximants U D x)), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
intros bot H'1; elim H'1; intros H'2 H'3; clear H'1.
(* Goal: Inhabited U (Approximants U D x) *)
(* Goal: forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) (Approximants U D x)), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
apply Inhabited_intro with (x := bot); auto with sets.
(* Goal: In U (Approximants U D y) c *)
apply Defn_of_Approximants; auto with sets.
(* Goal: Rel_of U D bot x *)
(* Goal: forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) (Approximants U D x)), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
elim H'2; auto with sets.
(* Goal: forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) (Approximants U D x)), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
intros x1 x2 H'1; red in H'1; auto with sets.
generalize (H'1 x1); intro h; lapply h;
 [ intro H'2; clear h | clear h; try assumption ]; 
 auto 20 with sets.
generalize (H'1 x2); intro h; lapply h;
 [ intro H'3; clear h | clear h; try assumption ]; 
 auto 20 with sets.
(* Goal: @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
elim H'3.
(* Goal: forall (c : U) (_ : Compact U D c) (_ : Rel_of U D c x), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 c) x3)) *)
intros c H'4 H'5.
(* Goal: @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 c) x3)) *)
elim H'2.
(* Goal: forall (c0 : U) (_ : Compact U D c0) (_ : Rel_of U D c0 x), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U c0 c) x3)) *)
intros c' H'6 H'7.
(* Goal: @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U c' c) x3)) *)
cut (Compatible U D c' c).
(* Goal: forall _ : Compatible U D c' c, @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U c' c) x3)) *)
(* Goal: Compatible U D c' c *)
intro H'8; try assumption.
lapply Lub_of_compacts_is_compact; [ intro H'9; elim (H'9 c' c x) | idtac ];
 auto with sets.
(* Goal: forall (x0 : U) (_ : and (Lub U D (Couple U c' c) x0) (Approximant U D x x0)), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U c' c) x3)) *)
(* Goal: Included U (Couple U c' c) (Approximants U D x) *)
(* Goal: Compatible U D c' c *)
intros x0 H'10; elim H'10; intros H'11 H'12; elim H'11; clear H'10.
(* Goal: forall (_ : Upper_Bound U D (Couple U c' c) x0) (_ : forall (y : U) (_ : Upper_Bound U D (Couple U c' c) y), Rel_of U D x0 y), @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U c' c) x3)) *)
(* Goal: Included U (Couple U c' c) (Approximants U D x) *)
(* Goal: Compatible U D c' c *)
intros H'10 H'13; exists x0; split; auto with sets.
(* Goal: In U (Approximants U D x) x0 *)
(* Goal: Included U (Couple U c' c) (Approximants U D x) *)
(* Goal: Compatible U D c' c *)
elim H'12; auto with sets.
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
red in |- *; simpl in |- *.
(* Goal: forall (x0 : U) (_ : In U (Couple U c' c) x0), In U (Approximants U D x) x0 *)
(* Goal: Compatible U D c' c *)
intros x0 H'10; elim H'10; auto with sets.
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
red in |- *; simpl in |- *.
(* Goal: forall (_ : In U (Carrier_of U D) c') (_ : In U (Carrier_of U D) c), @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U c' c) z)) *)
intros H'8 H'9; exists x; auto with sets.
Qed.

Theorem Inclusion_of_Approximants :
 Domain U D ->
 forall x y : U,
 In U (Carrier_of U D) x ->
 In U (Carrier_of U D) y ->
 Included U (Approximants U D x) (Approximants U D y) -> Rel_of U D x y.
Proof.
(* Goal: forall (_ : Domain U D) (x y : U) (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) y) (_ : Included U (Approximants U D x) (Approximants U D y)), Rel_of U D x y *)
intros H' x y H'0 H'1 H'2; try assumption; auto with sets.
(* Goal: @ex U (fun bsup : U => and (Lub U D (Union U A (Singleton U x0)) bsup) (Approximant U D x bsup)) *)
red in H'; elim H'; intros H'3 H'4; clear H'; red in H'4.
(* Goal: Rel_of U D x y *)
elim H'4; intros H' H'5; clear H'4; red in H'; auto with sets.
generalize (H' x); intro h; elim h; intros H'4 H'6; clear h; elim H'6;
 auto with sets.
clear H'6; intros H'7 H'8; apply H'8.
generalize (H' y); intro h; elim h; intros H'6 H'9; clear h; try exact H'9;
 auto with sets.
(* Goal: Upper_Bound U D (Approximants U D x) y *)
apply Upper_downward_stable with (Approximants U D y); auto with sets.
(* Goal: Included U (Approximants U D y) (Carrier_of U D) *)
(* Goal: Upper_Bound U D (Approximants U D y) y *)
red in |- *; (intros x0 H'10; elim H'10); auto with sets.
(* Goal: Included U (Approximants U D y) (Carrier_of U D) *)
(* Goal: Upper_Bound U D (Approximants U D y) y *)
red in |- *; (intros x0 H'10; elim H'10); auto with sets.
(* Goal: Upper_Bound U D (Approximants U D y) y *)
apply Upper_Bound_definition; auto with sets.
(* Goal: forall (y0 : U) (_ : In U (Approximants U D y) y0), Rel_of U D y0 y *)
intros y0 H'10; elim H'10; auto with sets.
Qed.
Hint Resolve Inclusion_of_Approximants.

Theorem Less_imp_Inclusion_of_Approximants :
 Domain U D ->
 forall x y : U,
 In U (Carrier_of U D) x ->
 In U (Carrier_of U D) y ->
 Rel_of U D x y -> Included U (Approximants U D x) (Approximants U D y).
Proof.
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
intros H' x y H'0 H'1 H'2; red in |- *; simpl in |- *.
(* Goal: @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
intros x0 H'3; elim H'3.
(* Goal: forall (c : U) (_ : Compact U D c) (_ : Rel_of U D c x), In U (Approximants U D y) c *)
generalize Rel_of_transitive; intro RoT; red in RoT.
(* Goal: forall (c : U) (_ : Compact U D c) (_ : Rel_of U D c x), In U (Approximants U D y) c *)
intros c H'4 H'5; try assumption.
(* Goal: In U (Approximants U D y) c *)
apply Defn_of_Approximants; auto with sets.
(* Goal: Rel_of U D c y *)
apply RoT with (y := x); auto with sets.
Qed.

Theorem Approximants_define_element :
 Domain U D ->
 forall x y : U,
 In U (Carrier_of U D) x ->
 In U (Carrier_of U D) y -> Approximants U D x = Approximants U D y -> x = y.
(* Goal: forall (_ : Domain U D) (x y : U) (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) y) (_ : @eq (Ensemble U) (Approximants U D x) (Approximants U D y)), @eq U x y *)
intros H' x y H'0 H'1 H'2; try assumption.
(* Goal: @eq U x y *)
cut (Same_set U (Approximants U D x) (Approximants U D y)).
(* Goal: @ex U (fun x3 : U => and (In U (Approximants U D x) x3) (Upper_Bound U D (Couple U x1 x2) x3)) *)
intro H'3; elim H'3.
(* Goal: forall (_ : Included U (Approximants U D x) (Approximants U D y)) (_ : Included U (Approximants U D y) (Approximants U D x)), @eq U x y *)
(* Goal: Same_set U (Approximants U D x) (Approximants U D y) *)
generalize (Rel_of_antisymmetric U D); auto with sets.
(* Goal: Same_set U (Approximants U D x) (Approximants U D y) *)
rewrite H'2; auto with sets.
Qed.
Hint Resolve Approximants_define_element.
Require Import Classical_sets.
Hint Unfold not.

Theorem Corollary1_1 :
 Domain U D ->
 forall x y : U,
 Compact U D x ->
 In U (Carrier_of U D) y ->
 Strict_Rel_of U D x y ->
 exists z : U, In U (Approximants U D y) z /\ Strict_Rel_of U D x z.
Proof.
(* Goal: forall (_ : Domain U D) (x y : U) (_ : Compact U D x) (_ : In U (Carrier_of U D) y) (_ : Strict_Rel_of U D x y), @ex U (fun z : U => and (In U (Approximants U D y) z) (Strict_Rel_of U D x z)) *)
unfold Strict_Rel_of in |- *.
(* Goal: forall (_ : Domain U D) (x y : U) (_ : Compact U D x) (_ : In U (Carrier_of U D) y) (_ : and (Rel_of U D x y) (not (@eq U x y))), @ex U (fun z : U => and (In U (Approximants U D y) z) (and (Rel_of U D x z) (not (@eq U x z)))) *)
intros H' x y H'0 H'1 H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
lapply Less_imp_Inclusion_of_Approximants;
 [ intro H'2; lapply (H'2 x y);
    [ intro H'7; lapply H'7;
       [ intro H'8; lapply H'8;
          [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ]
       | clear H'7 ]
    | idtac ]
 | idtac ]; auto with sets.
elim
 (Strict_super_set_contains_new_element U (Approximants U D x)
    (Approximants U D y)); auto 8 with sets.
(* Goal: forall (x0 : U) (_ : In U (Setminus U (Approximants U D y) (Approximants U D x)) x0), @ex U (fun z : U => and (In U (Approximants U D y) z) (and (Rel_of U D x z) (not (@eq U x z)))) *)
intros x0 H'5; elim H'5; clear H'5.
(* Goal: forall (_ : In U (Approximants U D y) x0) (_ : not (In U (Approximants U D x) x0)), @ex U (fun z : U => and (In U (Approximants U D y) z) (and (Rel_of U D x z) (not (@eq U x z)))) *)
intro H'5; elim H'5; clear H'5.
(* Goal: forall (c : U) (_ : Compact U D c) (_ : Rel_of U D c y) (_ : not (In U (Approximants U D x) c)), @ex U (fun z : U => and (In U (Approximants U D y) z) (and (Rel_of U D x z) (not (@eq U x z)))) *)
intros c H'5 H'6 H'7; try assumption.
lapply Lub_of_compacts_is_compact; [ intro H'8; elim (H'8 x c y) | idtac ];
 auto with sets.
(* Goal: forall (x0 : U) (_ : and (Lub U D (Couple U x c) x0) (Approximant U D y x0)), @ex U (fun z : U => and (In U (Approximants U D y) z) (and (Rel_of U D x z) (not (@eq U x z)))) *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
intros x1 H'11; elim H'11; intros H'12 H'13; elim H'12; clear H'11.
(* Goal: forall (_ : Upper_Bound U D (Couple U x c) x1) (_ : forall (y : U) (_ : Upper_Bound U D (Couple U x c) y), Rel_of U D x1 y), @ex U (fun z : U => and (In U (Approximants U D y) z) (and (Rel_of U D x z) (not (@eq U x z)))) *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
intros H'11 H'14; exists x1.
(* Goal: and (In U (Approximants U D y) x1) (and (Rel_of U D x x1) (not (@eq U x x1))) *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
split; [ idtac | split; [ try assumption | idtac ] ]; auto with sets.
(* Goal: In U (Approximants U D y) x1 *)
(* Goal: Rel_of U D x x1 *)
(* Goal: not (@eq U x x1) *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
elim H'13; auto with sets.
(* Goal: Rel_of U D x x1 *)
(* Goal: not (@eq U x x1) *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
elim H'11; auto with sets.
(* Goal: not (@eq U x x1) *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
red in |- *; simpl in |- *; intro H'15; try exact H'15.
(* Goal: False *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
apply H'7.
(* Goal: In U (Approximants U D x) c *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
rewrite H'15; auto with sets.
elim (Upper_Bound_Couple_inv U D x c x1);
 [ intros H'21 H'22; elim H'22; intros H'23 H'24; try exact H'23; clear H'22
 | idtac ]; auto with sets.
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
red in |- *; simpl in |- *.
(* Goal: Rel_of U D x x1 *)
(* Goal: not (@eq U x x1) *)
(* Goal: Included U (Couple U x c) (Approximants U D y) *)
(* Goal: Conditionally_complete U D *)
intros x1 H'11; elim H'11; auto with sets.
(* Goal: Conditionally_complete U D *)
apply Coherent_implies_Conditionally_Complete.
(* Goal: Conditionally_complete U D *)
elim H'; auto with sets.
Qed.

Theorem Corollary1_2 :
 Domain U D ->
 forall x : U,
 In U (Carrier_of U D) x ->
 ~ Compact U D x -> ~ Finite U (Approximants U D x).
(* Goal: forall (_ : Domain U D) (x : U) (_ : In U (Carrier_of U D) x) (_ : not (Compact U D x)), not (Finite U (Approximants U D x)) *)
intros H' x H'0 H'1; red in |- *; simpl in |- *; intro H'2; try exact H'2.
(* Goal: False *)
apply H'1.
lapply approximants_closed_by_finite_lubs;
 [ intro H'3; elim (H'3 x (Approximants U D x)) | idtac ]; 
 auto with sets.
(* Goal: forall (x0 : U) (_ : and (Lub U D (Approximants U D x) x0) (Approximant U D x x0)), Compact U D x *)
(* Goal: Conditionally_complete U D *)
intros x0 H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
(* Goal: Compact U D x *)
(* Goal: Conditionally_complete U D *)
elim H'.
(* Goal: forall (_ : Coherent U D) (_ : Omega_algebraic U D), Compact U D x *)
(* Goal: Conditionally_complete U D *)
intros H'4 H'7; elim H'7.
(* Goal: forall (_ : Algebraic U D) (_ : Denumerable U (fun x : U => Compact U D x)), Compact U D x *)
(* Goal: Conditionally_complete U D *)
intro H'9; red in H'9.
(* Goal: forall _ : Denumerable U (fun x : U => Compact U D x), Compact U D x *)
(* Goal: Conditionally_complete U D *)
elim (H'9 x); intros H'11 H'12; try exact H'12.
(* Goal: forall _ : Denumerable U (fun x : U => Compact U D x), Compact U D x *)
(* Goal: Conditionally_complete U D *)
intro H'10; clear H'10.
lapply (Lub_is_unique U D);
 [ intro H'14; rewrite (H'14 (Approximants U D x) x x0) | idtac ];
 auto with sets.
(* Goal: Compact U D x0 *)
(* Goal: Conditionally_complete U D *)
elim H'6; auto with sets.
(* Goal: Conditionally_complete U D *)
elim H'; auto with sets.
Qed.
End Advanced_lemmas.
Hint Resolve Inclusion_of_Approximants.
Hint Resolve Upper_Bound_Couple_intro.
