Require Import Classical.
Require Import Classical_Pred_Type.
Require Import Coq.Reals.Reals.

Require Import Tactics.
Require Import Automation.
Require Import Notations.Common.
Require Import Notations.Reals.
Require Import Chains.
Require Import Notations.Sets.

Open Scope R_scope.

Waterproof Enable Automation RealsAndIntegers.

Open Scope subset_scope.
Definition is_upper_bound (A : subset ℝ) (M : ℝ) :=
  ∀ a ∈ A, a ≤ M.

Definition is_bounded_above (A : subset R) :=
  ∃ M ∈ ℝ, is_upper_bound A M.

Definition is_sup (A : subset R) (M : ℝ) :=
  is_upper_bound A M ∧ ∀ L ∈ ℝ, is_upper_bound A L ⇒ M ≤ L.


Lemma is_upper_bound_Raxioms_is_upper_bound_iff (A : subset ℝ) (M : ℝ) :
  is_upper_bound A M <-> Raxioms.is_upper_bound A M.
Proof.
  reflexivity.
Qed.

Lemma bdd_above_bound_iff (A : subset ℝ) :
  is_bounded_above A <-> bound A.
Proof.
  unfold is_bounded_above, bound.
  By (exists_exists_in_iff) we conclude that
    ((∃ M ∈ R, is_upper_bound A M) <-> ∃ m : ℝ, Raxioms.is_upper_bound A m).
Qed.

Lemma is_sup_is_lub_iff (A : subset ℝ) (M : ℝ) :
  is_lub A M <-> is_sup A M.
Proof.
  unfold is_lub, is_sup.
  split.
  * intros [H1 H2].
    split.
    + auto using bdd_above_bound_iff.
    + intros L HL.
      apply H2.
  * intros [H1 H2].
    split.
    + assumption.
    + intro b.
      apply H2.
      apply mem_subset_full_set.
Qed.

Notation "M 'is' 'the' '_supremum_' 'of' A" := (is_sup A M) (at level 69).
Notation "M 'is' 'the' 'supremum' 'of' A" := (is_sup A M) (at level 69, only parsing).
Local Ltac2 unfold_is_sup (statement : constr) := eval unfold is_sup in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "supremum" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_sup (Some "supremum") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "supremum" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_sup (Some "supremum") false x.

Notation "A 'is' '_bounded' 'from' 'above_'" := (is_bounded_above A) (at level 69).
Notation "A 'is' 'bounded' 'from' 'above'" := (is_bounded_above A) (at level 69, only parsing).
Local Ltac2 unfold_bound (statement : constr) := eval unfold is_bounded_above in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "bounded" "from" "above" x(opt(seq("in", constr))) :=
  wp_unfold unfold_bound (Some "bounded from above") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "bounded" "from" "above" x(opt(seq("in", constr))) :=
  wp_unfold unfold_bound (Some "bounded from above") false x.

Notation "M 'is' 'an' '_upper' 'bound_' 'for' A" := (is_upper_bound A M) (at level 69).
Notation "M 'is' 'an' 'upper' 'bound' 'for' A" := (is_upper_bound A M) (at level 69, only parsing).
Local Ltac2 unfold_is_upper_bound (statement : constr) := eval unfold is_upper_bound in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "upper" "bound" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_upper_bound (Some "upper bound") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "upper" "bound" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_upper_bound (Some "upper bound") false x.

Definition is_max (A : subset ℝ) (x : ℝ) := (x ∈ A) ∧ (x is an upper bound for A).

Notation "M 'is' 'the' '_maximum_' 'of' A" := (is_max A M) (at level 69).
Notation "M 'is' 'the' 'maximum' 'of' A" := (is_max A M) (at level 69, only parsing).
Local Ltac2 unfold_is_max (statement : constr) := eval unfold is_max in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "maximum" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_max (Some "maximum") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "maximum" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_max (Some "maximum") false x.

Lemma R_complete (A : ℝ → Prop) :
  ∀ a ∈ A, (A is bounded from above) ⇒ ∃ M ∈ ℝ, M is the supremum of A.
Proof.
    Take a ∈ A.
    Assume that (A is bounded from above) (i).
    It holds that (∃ M ∈ ℝ, is_upper_bound A M) (ii).
    We claim that (there exists x : ℝ, A x).
    { Choose (a). We conclude that (A a). }
    We claim that (bound A).     {
      Obtain M according to (ii).
      We need to show that (∃ m : ℝ, ∀ x : ℝ, x ∈ A -> x ≤ m).
      Choose m := M.
      Take x ∈ A.
      We conclude that (x ≤ m).
    }
    By completeness it holds that ({M | is_lub A M}).
    Obtain such an M.
    It holds that ((M is an upper bound for A) ∧
      (∀ L : ℝ, L is an upper bound for A ⇒ M ≤ L)).
    Choose (M).
    * Indeed, (M ∈ ℝ).
    * We need to show that ((M is an upper bound for A) ∧
        ∀ L ∈ ℝ, L is an upper bound for A ⇒ M ≤ L).
      We show both statements.
      + We conclude that (M is an upper bound for A).
      + We need to show that (∀ L ∈ ℝ, L is an upper bound for A ⇒ M ≤ L).
        Take L ∈ ℝ.
        We conclude that (L is an upper bound for A ⇒ M ≤ L).
Qed.

Lemma R_complete_unsealed : ∀ (A : ℝ → Prop), ∀ (a : ℝ),
  a ∈ A ⇒ (A is bounded from above) ⇒
  exists M : R, M ∈ R ∧ M is the supremum of A.
exact R_complete.
Qed.

Definition is_lower_bound (A : subset ℝ) (m : ℝ) :=
  ∀ a ∈ A, m ≤ a.

Definition is_bounded_below (A : subset ℝ) :=
  ∃ m ∈ ℝ, is_lower_bound A m.

Definition is_inf (A : subset ℝ) (m : ℝ) :=
  (is_lower_bound A m) ∧ (∀ l ∈ R, is_lower_bound A l ⇒ l ≤ m).

Notation "m 'is' 'the' '_infimum_' 'of' A" := (is_inf A m) (at level 69).
Notation "m 'is' 'the' 'infimum' 'of' A" := (is_inf A m) (at level 69, only parsing).
Local Ltac2 unfold_is_inf (statement : constr) := eval unfold is_inf in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "infimum" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_inf (Some "infimum") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "infimum" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_inf (Some "infimum") false x.

Notation "A 'is' '_bounded' 'from' 'below_'" := (is_bounded_below A) (at level 69).
Notation "A 'is' 'bounded' 'from' 'below'" := (is_bounded_below A) (at level 69, only parsing).
Local Ltac2 unfold_is_bounded_below (statement : constr) :=
  eval unfold is_bounded_below in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "bounded" "from" "below" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_bounded_below (Some "bounded from below") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "bounded" "from" "below" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_bounded_below (Some "bounded from below") false x.

Notation "M 'is' 'a' '_lower' 'bound_' 'for' A" := (is_lower_bound A M) (at level 69).
Notation "M 'is' 'a' 'lower' 'bound' 'for' A" := (is_lower_bound A M) (at level 69, only parsing).
Local Ltac2 unfold_is_lower_bound (statement : constr) := eval unfold is_lower_bound in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "lower" "bound" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_lower_bound (Some "lower bound") true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "lower" "bound" x(opt(seq("in", constr))) :=
  wp_unfold unfold_is_lower_bound (Some "lower bound") false x.

Definition set_opp (A : ℝ -> Prop) := (fun x ↦ (A (-x))).

Lemma upp_bd_set_to_low_bd_set_opp :
  ∀ (A : ℝ → Prop), ∀ M ∈ ℝ,
    M is an upper bound for A ⇒
      is_lower_bound (set_opp A) (-M).
Proof.
    Take A : (ℝ → Prop).
    Take M ∈ ℝ.
    Assume that (M is an upper bound for A) (i).
    We need to show that (∀ b : ℝ, (set_opp A b) ⇒ -M ≤ b).
    Take b : ℝ. Assume that (set_opp A b).
    Define a := (-b).
    It holds that (A a).
    By (i) it holds that (a ≤ M).
    We conclude that (-M ≤ b).
Qed.

Lemma low_bd_set_to_upp_bd_set_opp :
  ∀ (A : ℝ → Prop), ∀ m ∈ ℝ,
    is_lower_bound A m ⇒
      -m is an upper bound for (set_opp A).
Proof.
    Take A : (ℝ → Prop).
    Take m ∈ ℝ.
    Assume that (is_lower_bound A m) (i).
    We need to show that (for all b : ℝ, (set_opp A b) ⇒ b ≤ -m).
    Take b : ℝ. Assume that (set_opp A b).
    Define a := (-b).
    By (i) it holds that (m ≤ a).
    We conclude that (& b = -a <= -m).
Qed.

Lemma low_bd_set_opp_to_upp_bd_set :
  ∀ (A : ℝ → Prop), ∀ m ∈ ℝ,
    is_lower_bound (set_opp A) m ⇒
      -m is an upper bound for A.
Proof.
    Take A : (ℝ → Prop).
    Take m ∈ ℝ.
    Assume that (is_lower_bound (set_opp A) m).
    We need to show that (∀ a : ℝ, (A a) ⇒ a ≤ -m).
    Take a : ℝ. Assume that (A a).
    It holds that (for all b : ℝ, (set_opp A b) ⇒ m ≤ b).
    We claim that (A (--a)).
    { It holds that (--a = a) (ii).
      It holds that (A a) (iii).
      exact (eq_ind_r(_,_,A,(iii),_,(ii))).
    }
    It holds that ((set_opp A) (-a)).
    Define b := (-a).
    It holds that (m ≤ b).
    It holds that (m ≤ -a).
    We conclude that (a ≤ - m).
Qed.

Lemma upp_bd_set_opp_to_low_bd_set :
  ∀ (A : ℝ → Prop), ∀ M ∈ ℝ,
    is_upper_bound (set_opp A) M ⇒
      is_lower_bound A (-M).
Proof.
    Take A : (ℝ → Prop).
    Take M ∈ ℝ.
    Assume that (is_upper_bound (set_opp A) M) (i).
    We need to show that (∀ a : ℝ, (A a) ⇒ -M ≤ a).
    Take a : ℝ. Assume that (A a).
    We claim that (A (--a)).
    { It holds that (--a = a) (ii).
      It holds that (A a) (iii).
      exact (eq_ind_r(_,_,A,(iii),_,(ii))).
    }
    It holds that ((set_opp A) (-a)).
    Define b := (-a).
    By (i) it holds that (b ≤ M).
    It holds that (-a ≤ M).
    We conclude that (- M ≤ a).
Qed.

Lemma bdd_below_to_bdd_above_set_opp :
  ∀ (A : ℝ → Prop),
    is_bounded_below A ⇒ is_bounded_above (set_opp A).
Proof.
    Take A : (ℝ → Prop).
    Assume that (is_bounded_below A) (i).
    We need to show that (∃ M ∈ ℝ, is_upper_bound (set_opp A) M).
    By (i) it holds that (∃ m ∈ ℝ, is_lower_bound A m).
    Obtain such an m.
    Choose M := (-m).
    * Indeed, (M ∈ ℝ).
    * By low_bd_set_to_upp_bd_set_opp we conclude that (is_upper_bound (set_opp A) (M)).
Qed.

Lemma sup_set_opp_is_inf_set :
  ∀ (A : ℝ → Prop), ∀ M ∈ ℝ,
    is_sup (set_opp A) M ⇒ is_inf A (-M).
Proof.
    Take A : (ℝ → Prop).
    Take M ∈ ℝ.
    Assume that (is_sup (set_opp A) M).
    It holds that (is_upper_bound (set_opp A) M
        ∧ (for all M0 : ℝ, M0 ∈ ℝ -> is_upper_bound (set_opp A) M0 ⇨ M ≤ M0)) (i).
    Because (i) both (is_upper_bound (set_opp A) M) and
      (for all M0 : ℝ, M0 ∈ ℝ -> is_upper_bound (set_opp A) M0 ⇨ M ≤ M0) hold.
    We need to show that
      (is_lower_bound A (- M) ∧ (∀ l ∈ ℝ, is_lower_bound A l ⇨ l ≤ -M)).
    We show both statements.
    - We need to show that (is_lower_bound A (- M)).
      We claim that (is_upper_bound (set_opp A) M).
      We need to show that (for all a : ℝ, (set_opp A a) ⇒ a ≤ M).
      Take a : ℝ. Assume that (set_opp A a).
      It holds that (for all x : ℝ, (set_opp A x) ⇒ x ≤ M) (ii).
      By (ii) it holds that (is_upper_bound (set_opp A) M).
      We conclude that (a <= M).

      By upp_bd_set_opp_to_low_bd_set we conclude that (is_lower_bound A (-M)).

    - We need to show that (∀ l ∈ ℝ, is_lower_bound A l ⇒ l ≤ -M).
      Take l ∈ ℝ.
      Assume that (is_lower_bound A l).
      It holds that (is_upper_bound (set_opp A) M
        ∧ (for all M0 : ℝ, M0 ∈ ℝ -> is_upper_bound (set_opp A) M0 ⇨ M ≤ M0)).
      It holds that (∀ b : ℝ, b ∈ ℝ -> is_upper_bound (set_opp A) b ⇒ M ≤ b) (ii).
      By low_bd_set_to_upp_bd_set_opp it holds that (is_upper_bound (set_opp A) (-l)).
      By (ii) it holds that (M ≤ -l).
      We conclude that (l ≤ - M).
Qed.

Lemma exists_inf :
  ∀ (A : ℝ → Prop), ∀ x ∈ A, is_bounded_below A ⇒
    ∃ m ∈ ℝ, is_inf A m.
Proof.
    Take A : (ℝ → Prop).
    To show : (for all z : ℝ,
      A(z) ⇨ A is _bounded from below_ ⇨ ∃ m ∈ ℝ, m is the _infimum_ of A).
    Take z : ℝ. Assume that (A z).
    Assume that (is_bounded_below A) (vi).
    Define B := (set_opp A).
    We claim that (is_bounded_above B) (i).
    { By bdd_below_to_bdd_above_set_opp it suffices to show that (is_bounded_below A).
      We conclude that (is_bounded_below A).
    }
    We claim that (A (--z)).
    { It holds that (--z = z) (ii).
      It holds that (A z) (iii).
      exact (eq_ind_r(_,_,A,(iii),_,(ii))).
    }
    It holds that ((set_opp A) (-z)) (iv).
    It holds that (B (-z)).
    By R_complete it holds that (∃ M ∈ ℝ, is_sup B M).
    Obtain such an M.
    Choose m := (- M).
    * Indeed, (m ∈ ℝ).
    * By sup_set_opp_is_inf_set we conclude that (is_inf A m).
Qed.

Lemma sup_is_upp_bd :
  ∀ A : (ℝ → Prop),
    ∀ M ∈ ℝ,
      is_sup A M ⇒ is_upper_bound A M.
Proof.
    Take A : (ℝ → Prop).
    Take M ∈ ℝ.
    Assume that (is_sup A M).
    It holds that (is_upper_bound A M
      ∧ (∀ b ∈ ℝ, is_upper_bound A b ⇨ M ≤ b)) (i).
    Because (i) both (is_upper_bound A M) and
      (∀ M0 ∈ ℝ, is_upper_bound A M0 ⇨ M ≤ M0) hold.
    It follows that (is_upper_bound A M).
Qed.

Lemma any_upp_bd_ge_sup :
  ∀ A : (ℝ → Prop),
    ∀ M ∈ ℝ, ∀ L ∈ ℝ,
      is_sup A M ⇒ (is_upper_bound A L ⇒ M ≤ L).
Proof.
    Take A : (ℝ → Prop).
    Take M ∈ ℝ.
    Take L ∈ ℝ.
    Assume that (is_sup A M) (i).
    Assume that (is_upper_bound A L).
    Because (i) both (is_upper_bound A M) and
      (∀ M0 ∈ ℝ, is_upper_bound A M0 ⇨ M ≤ M0) hold.

    We conclude that (M ≤ L).
Qed.

Lemma inf_is_low_bd :
  ∀ A : (ℝ → Prop),
    ∀ m ∈ ℝ,
      is_inf A m ⇒ is_lower_bound A m.
Proof.
    Take A : (ℝ → Prop).
    Take m ∈ R.
    Assume that (is_inf A m) (i).
    Because (i) both (is_lower_bound A m) (ii) and
      (∀ M0 ∈ ℝ, is_lower_bound A M0 ⇨ M0 ≤ m) hold.
    By (ii) we conclude that (is_lower_bound A m).
Qed.

Lemma any_low_bd_le_inf :
  ∀ A : (ℝ → Prop),
    ∀ m ∈ ℝ, ∀ l ∈ ℝ,
      is_inf A m ⇒ is_lower_bound A l ⇒ l ≤ m.
Proof.
    Take A : (ℝ → Prop).
    Take m ∈ ℝ.
    Take l ∈ ℝ.
    Assume that (is_inf A m) (i).
    Assume that (is_lower_bound A l).
    Because (i) both (is_lower_bound A m) and
      (∀ M0 ∈ ℝ, is_lower_bound A M0 ⇨ M0 ≤ m) hold.
    We conclude that (l ≤ m).
Qed.

Lemma exists_almost_maximizer :
  ∀ (A : ℝ → Prop), ∀ M ∈ ℝ,
    is_sup A M ⇒
      ∀ (L : ℝ), L < M ⇒
        ∃ a ∈ A, L < a.
Proof.
    Take A : (ℝ → Prop).
    Take M ∈ ℝ.
    Assume that (is_sup A M).
    Take L : ℝ.
    Assume that (L < M).
    We argue by contradiction.
    Assume that (¬ (there exists a : ℝ, (A a) ∧ L < a)) (i).
    It holds that (∀ x : ℝ, (A x) ⇒ x <= L) (ii).
    By (ii) it holds that (is_upper_bound A L).

    By any_upp_bd_ge_sup it holds that (M <= L).
    It holds that (¬(M ≤ L)).
    Contradiction.
Qed.

Lemma exists_almost_minimizer :
  ∀ (A : ℝ → Prop), ∀ m ∈ ℝ,
    is_inf A m ⇒
      ∀ L > m,
        ∃ a ∈ A, a < L.
Proof.
    Take A : (ℝ → Prop).
    Take m ∈ ℝ.
    Assume that (is_inf A m).
    Take L : ℝ.
    Assume that (L > m).
    We argue by contradiction.
    Assume that (¬ (there exists a : ℝ, (A a) ∧ L > a)).
    It holds that (∀ x : ℝ, (A x) ⇒ L ≤ x) (i).
    By (i) it holds that (is_lower_bound A L).

    By any_low_bd_le_inf it holds that (L <= m).
    It holds that (¬(L ≤ m)).
    Contradiction.
Qed.

Lemma if_almost_maximizer_then_every_upp_bd_larger :
  ∀ (A : ℝ → Prop), ∀ M ∈ ℝ,
    (∀ (L : ℝ), L < M ⇒ ∃ a ∈ A, L < a)
       ⇒ ∀ K ∈ ℝ, is_upper_bound A K ⇒ M ≤ K.
Proof.
Take A : (ℝ → Prop) and M ∈ ℝ.
Assume that (∀ L : ℝ, L < M ⇒ there exists a : ℝ, (A a) ∧ L < a) (i).
Take K ∈ ℝ.
Assume that (is_upper_bound A K).
It holds that (∀ a : ℝ, (A a) ⇒ a ≤ K) (ii).
We need to show that (M ≤ K).
We argue by contradiction.
Assume that (¬ M ≤ K).
It holds that (M > K).
By (i) it holds that (∃ a : ℝ, (A a) ∧ K < a).
Obtain such an a. It holds that ((A a) ∧ (K < a)) (iii).
Because (iii) both (A a) and (K < a) hold.
By (ii) it holds that (a ≤ K).
It holds that (K < K).
It holds that (¬ (K < K)).
Contradiction.
Qed.

Lemma if_almost_minimizer_then_every_low_bd_smaller :
  ∀ (A : ℝ → Prop), ∀ m ∈ ℝ,
    (∀ L > m, ∃ a ∈ A, a < L)
       ⇒ ∀ K ∈ ℝ, is_lower_bound A K ⇒ K ≤ m.
Proof.
Take A : (ℝ → Prop) and m ∈ ℝ.
Assume that (∀ L : ℝ, L > m ⇒ there exists a : ℝ, (A a) ∧ L > a) (i).
Take K ∈ ℝ.
Assume that (is_lower_bound A K).
It holds that (∀ a : ℝ, (A a) ⇒ K ≤ a) (ii).
We need to show that (K ≤ m).
We argue by contradiction.
Assume that (¬ K ≤ m).
It holds that (K > m).
By (i) it holds that (∃ a : ℝ, (A a) ∧ K > a).
Obtain such an a. It holds that ((A a) ∧ (K > a)) (iii).
Because (iii) both (A a) and (K > a) hold.
By (ii) it holds that (K ≤ a).
It holds that (K > K).
It holds that (¬ (K > K)).
Contradiction.
Qed.

Lemma if_almost_maximizer_ε_then_every_upp_bd_larger :
  ∀ (A : ℝ → Prop), ∀ M ∈ ℝ,
    (∀ ε > 0, ∃ a ∈ A, M - ε < a)
       ⇒ ∀ K ∈ ℝ, is_upper_bound A K ⇒ M ≤ K.
Proof.
  Take A : (ℝ → Prop) and M ∈ ℝ.
  Assume that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ M - ε < a) (i).
  Take K ∈ ℝ.
  apply if_almost_maximizer_then_every_upp_bd_larger.
  * We conclude that (M ∈ ℝ).
  * Take L : ℝ; such that (L < M).
    It holds that (M - L > 0).
    Define ε1 := (M - L).
    It holds that (ε1 > 0).
    By (i) it holds that (there exists a : ℝ, (A a) ∧ M - ε1 < a).
    Obtain such an a. It holds that ((A a) ∧ (M - ε1 < a)) (ii).
    Because (ii) both (A a) and (M - ε1 < a) hold.
    Choose (a).
    + Indeed, (a ∈ A).
    + We conclude that (& L = M - (M - L) = M - ε1 < a).
  * We conclude that (K ∈ ℝ).
Qed.

Lemma if_almost_minimizer_ε_then_every_low_bd_smaller :
  ∀ (A : ℝ → Prop), ∀ m ∈ ℝ,
    (∀ ε > 0, ∃ a ∈ A, m + ε > a)
       ⇒ ∀ K ∈ ℝ, is_lower_bound A K ⇒ K ≤ m.
Proof.
  Take A : (ℝ → Prop) and m ∈ ℝ.
  Assume that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a) (i).
  Take K ∈ ℝ.
  apply if_almost_minimizer_then_every_low_bd_smaller.
  * We conclude that (m ∈ ℝ).
  * Take L : ℝ; such that (L > m).
    It holds that (L - m > 0).
    Define ε1 := (L - m).
    It holds that (ε1 > 0).
    By (i) it holds that (there exists a : ℝ, (A a) ∧ m + ε1 > a).
    Obtain such an a. It holds that ((A a) ∧ (m + ε1 > a)) (ii).
    Choose (a).
    - Indeed, (a ∈ A).
    - We conclude that (& a < m + ε1 = m + L - m = L).
  * We conclude that (K ∈ ℝ).
Qed.

Lemma exists_almost_maximizer_ε :
  ∀ (A : ℝ → Prop), ∀ M ∈ ℝ,
    is_sup A M ⇒
      ∀ ε > 0, ∃ a ∈ A, M - ε < a.
Proof.
    Take A : (ℝ → Prop).
    Take M ∈ ℝ.
    Assume that (is_sup A M).
    Take ε : ℝ; such that (ε > 0).
    It holds that (M - ε < M).

    apply exists_almost_maximizer with (L := M- ε) (M := M).
    - We conclude that (M ∈ ℝ).
    - We conclude that (is_sup A M).
    - We conclude that (M - ε < M).
Qed.

Lemma exists_almost_minimizer_ε :
  ∀ (A : ℝ → Prop), ∀ m ∈ ℝ,
    is_inf A m ⇒
      ∀ ε > 0, ∃ a ∈ A, a < m + ε.
Proof.
    Take A : (ℝ → Prop).
    Take m ∈ ℝ.
    Assume that (is_inf A m).
    Take ε : ℝ; such that (ε > 0).
    It holds that (m + ε > m).

    apply exists_almost_minimizer with (L := m + ε) (m := m).
    - We conclude that (m ∈ ℝ).
    - We conclude that (is_inf A m).
    - We conclude that (m + ε > m).
Qed.

Definition is_sup_alt_char (A : ℝ → Prop) (M : ℝ) :=
  is_upper_bound A M ∧ (∀ ε > 0, ∃ a ∈ A, M - ε < a).

Definition is_inf_alt_char (A : ℝ → Prop) (m : ℝ) :=
  is_lower_bound A m ∧ (∀ ε > 0, ∃ a ∈ A, a < m + ε).

Theorem alt_char_sup (A : ℝ → Prop) (M : ℝ) :
    is_sup A M ⇔ is_sup_alt_char A M.
Proof.
  We show both directions.
  - We need to show that (is_sup A M ⇨ is_sup_alt_char A M).
    Assume that (is_sup A M).
    We need to show that (
    is_upper_bound A M
    ∧ (for all ε : ℝ,
      ε > 0 ⇨ there exists a : ℝ, (A a) ∧
                M - ε < a) ).
    We show both statements.
    + We need to show that (is_upper_bound A M).
      It holds that (
      is_upper_bound A M
      ∧ (∀ M0 ∈ ℝ,
        is_upper_bound A M0 ⇨ M ≤ M0) ) (i).
      Because (i) both (is_upper_bound A M) and
        (∀ M0 ∈ ℝ, is_upper_bound A M0 ⇨ M ≤ M0) hold.
      It follows that (is_upper_bound A M).

    + We need to show that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ M - ε < a ).
      apply exists_almost_maximizer_ε.
      * We conclude that (M ∈ ℝ).
      * We conclude that (M is the supremum of A).

  - We need to show that (is_sup_alt_char A M ⇨ is_sup A M).
    Assume that (is_sup_alt_char A M).
    It holds that (
    is_upper_bound A M
    ∧ (for all ε : ℝ,
      ε > 0 ⇨ there exists a : ℝ, (A a) ∧
                M - ε < a) ) (i).
    Because (i) both (is_upper_bound A M) (ii) and
      (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ M - ε < a) (iii) hold.

    We need to show that (
    is_upper_bound A M
    ∧ (∀ M0 ∈ ℝ,
      is_upper_bound A M0 ⇨ M ≤ M0) ).
    We show both statements.
    + We need to show that (is_upper_bound A M).
      By (ii) we conclude that (is_upper_bound A M).
    + We need to show that (∀ M0 ∈ ℝ, is_upper_bound A M0 ⇨ M ≤ M0).
      Take M0 ∈ ℝ.
      apply if_almost_maximizer_ε_then_every_upp_bd_larger.
      * We conclude that (M ∈ ℝ).
      * By (iii) we conclude that (∀ ε > 0, ∃ a ∈ A, M - ε < a).
      * We conclude that (M0 ∈ ℝ).
Qed.

Theorem alt_char_inf (A : ℝ -> Prop) (m : ℝ) :
    is_inf A m ⇔ is_inf_alt_char A m.
Proof.
  We show both directions.
  - We need to show that (is_inf A m ⇨ is_inf_alt_char A m).
    Assume that (is_inf A m).
    We need to show that (
    is_lower_bound A m
    ∧ (for all ε : ℝ,
      ε > 0 ⇨ there exists a : ℝ, (A a) ∧
                m + ε > a) ).
    We show both statements.
    + We need to show that (is_lower_bound A m).
      It holds that (
      is_lower_bound A m ∧ (∀ l ∈ ℝ,
                          is_lower_bound A l ⇨ l ≤ m)
      ) (i).
      Because (i) both (is_lower_bound A m) and
        (∀ l ∈ ℝ, is_lower_bound A l ⇨ l ≤ m) hold.
      It follows that (is_lower_bound A m).

    + We need to show that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a).

      By exists_almost_minimizer_ε we conclude that
      (for all ε : ℝ,
        ε > 0 ⇨ there exists a : ℝ, (A a) ∧
              m + ε > a).

  - We need to show that (is_inf_alt_char A m ⇨ is_inf A m).
    Assume that (is_inf_alt_char A m).
    It holds that (
      is_lower_bound A m
      ∧ (for all ε : ℝ,
      ε > 0 ⇨ there exists a : ℝ, (A a) ∧
                m + ε > a) ) (i).
    Because (i) both (is_lower_bound A m) (ii) and
      (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a) hold.

    We need to show that (
      is_lower_bound A m ∧ (∀ l ∈ ℝ,
                          is_lower_bound A l ⇨ l ≤ m)
    ).
    We show both statements.
    + We need to show that (is_lower_bound A m).
      By (ii) we conclude that (is_lower_bound A m).
    + We need to show that (∀ l ∈ ℝ, is_lower_bound A l ⇨ l ≤ m).
      By if_almost_minimizer_ε_then_every_low_bd_smaller
      we conclude that (∀ l ∈ ℝ,
      is_lower_bound A l ⇨ l ≤ m).
Qed.

Lemma max_or_strict :
  ∀ (A : ℝ → Prop), ∀ M ∈ ℝ,
    is_sup A M ⇒
      (M ∈ A) ∨ (∀ a ∈ A, a < M).
Proof.
    Take A : (ℝ → Prop).
    Take M ∈ ℝ.
    Assume that (is_sup A M).
    We argue by contradiction.
    Assume that (¬ (A M ∨ (for all a : ℝ, (A a) ⇒ a < M))).
    It holds that ((¬ (A M)) ∧
      ¬(∀ a : ℝ, (A a) ⇒ a < M)) (i).
    Because (i) both(¬ (A M)) and (¬(∀ a : ℝ, (A a) ⇒ a < M)) hold.
    We claim that (for all a : ℝ, (A a) ⇒ a < M).
    {
      Take a : ℝ. Assume that (A a).
      By sup_is_upp_bd it holds that (is_upper_bound A M).
      It holds that (a ≤ M).
      We claim that (M ≠ a).
      {
        Assume that (M = a) (ii).
        We claim that (A M).
        { It holds that (A a) (iii).
      exact (eq_ind_r(_,_,A,(iii),_,(ii))).
        }
        Contradiction.
      }
      We conclude that (a < M).
    }
    Contradiction.
Qed.

Lemma bounded_by_upper_bound_propform
  (A : ℝ → Prop) (M : ℝ) (b : ℝ) :
  is_upper_bound A M ⇒ b ∈ A ⇒ b ≤ M.
Proof.
    Assume that (is_upper_bound A M) (i).
    Assume that (A b) (ii).
    We conclude that (b ≤ M).
Qed.

Lemma bounded_by_lower_bound_propform
  (A : ℝ → Prop) (m : ℝ) (b : ℝ) :
    is_lower_bound A m ⇒ b ∈ A ⇒ m ≤ b.
Proof.
    Assume that (is_lower_bound A m) (i).
    Assume that (A b) (ii).
    We conclude that (m ≤ b).
Qed.

Lemma seq_ex_almost_maximizer_ε :
  ∀ (a : ℕ → ℝ), ∀ (pr : has_ub a),
    ∀ ε > 0, ∃ k : ℕ, a k > lub a pr - ε.
Proof.
    Take a : (ℕ → ℝ).
    Assume that (has_ub a) (i).
    We need to show that (∀ ε > 0,
      there exists k : ℕ, a k > (let (a0, _) := ub_to_lub a (i) in a0) - ε).
    Define lub_a_prf := (ub_to_lub a (i)).
    We need to show that (∀ ε > 0, ∃ k, a(k) > (let (a0, _) := lub_a_prf in a0) - ε).
    clear _defeq. Obtain such an l.
    Take ε > 0.
    We claim that (is_sup (EUn a) l).
    {
      apply is_sup_is_lub_iff; assumption.
    }
    By exists_almost_maximizer_ε it holds that (∃ y : ℝ, (EUn a) y ∧ y > l - ε).
    Obtain such a y. It holds that ((EUn a) y ∧ y > l - ε) (iv).
    Because (iv) both (EUn a y) and (y > l - ε) hold.
    It holds that (there exists n : ℕ , y = a n).
    Obtain such an n.
    Choose k := n.
    simpl.
    We need to show that (l - ε < a n).
    We conclude that (& l - ε < y = a n).
Qed.

Lemma seq_ex_almost_maximizer_m :
  ∀ (a : ℕ → ℝ), ∀ (pr : has_ub a), ∀ (m : ℕ),
    ∃ k : ℕ, a k > lub a pr - 1 / (INR(m) + 1).
Proof.
    Take a : (ℕ → ℝ).
    Assume that (has_ub a).
    Take m : ℕ.
    apply seq_ex_almost_maximizer_ε.