From mathcomp Require Import ssreflect ssrbool eqtype seq.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]

(** * Computation of a Sequence's Supremum *)

(** This module provides a simple function [supremum] for the computation of a
    maximal element of a sequence, according to any given relation [R]. If the
    relation [R] is reflexive, total, and transitive, the result of [supremum]
    is indeed the supremum of the set of items in the sequence.  *)

Section SelectSupremum.

  (** Consider any type of elements with decidable equality... *)
  Context {T : eqType}.

  (** ...and any given relation [R]. *)
  Variable R : rel T.

  (** We first define a help function [choose_superior] that, given an element
      [x] and maybe a second element [y], picks [x] if [R x y] holds, and [y]
      otherwise. *)
  Definition choose_superior (x : T) (maybe_y : option T) : option T :=
    match maybe_y with
    | Some y => if R x y then Some x else Some y
    | None => Some x
    end.

  (** The supremum of a given sequence [s] can then be computed by simply
      folding [s] with [choose_superior]. *)
  Definition supremum (s : seq T) : option T := foldr choose_superior None s.

  (** Next, we establish that [supremum] satisfies its specification. To this
      end, we first establish a few simple helper lemmas. *)

  (** We start with observing how [supremum] can be unrolled one step. *)
  Lemma supremum_unfold:
    forall head tail,
      supremum (head :: tail) = choose_superior head (supremum tail).
T: eqType
R: rel T
forall (head : T) (tail : seq T),
supremum (head :: tail) =
choose_superior head (supremum tail)
  Proof.
T: eqType
R: rel T
forall (head : T) (tail : seq T),
supremum (head :: tail) =
choose_superior head (supremum tail)
    move=> head tail.
T: eqType
R: rel T
head: T
tail: seq T
supremum (head :: tail) =
choose_superior head (supremum tail)
    by rewrite [LHS]/supremum /foldr -/(foldr choose_superior None tail) -/(supremum tail).
  Qed.

  (** Next, we observe that [supremum] returns a result for any non-empty
      list. *)
  Lemma supremum_exists: forall x s, x \in s -> supremum s != None.
T: eqType
R: rel T
forall (x : T) (s : seq_predType T),
x \in s -> supremum s != None
  Proof.
T: eqType
R: rel T
forall (x : T) (s : seq_predType T),
x \in s -> supremum s != None
    move=> x s IN.
T: eqType
R: rel T
x: T
s: seq_predType T
IN: x \in s
supremum s != None
    elim: s IN; first by done.
T: eqType
R: rel T
x: T
forall (a : T) (l : seq T),
(x \in l -> supremum l != None) ->
x \in a :: l -> supremum (a :: l) != None
    move=> a l _ _.
T: eqType
R: rel T
x, a: T
l: seq T
supremum (a :: l) != None
    rewrite supremum_unfold.
T: eqType
R: rel T
x, a: T
l: seq T
choose_superior a (supremum l) != None
    destruct (supremum l); rewrite /choose_superior //.
T: eqType
R: rel T
x, a: T
l: seq T
s: T
(if R a s then Some a else Some s) != None
    by destruct (R a s).
  Qed.

  (** Conversely, if [supremum] finds nothing, then the list is empty. *)
  Lemma supremum_none: forall s, supremum s = None -> s = nil.
T: eqType
R: rel T
forall s : seq T, supremum s = None -> s = [::]
  Proof.
T: eqType
R: rel T
forall s : seq T, supremum s = None -> s = [::]
    move=> s.
T: eqType
R: rel T
s: seq T
supremum s = None -> s = [::]
    elim: s; first by done.
T: eqType
R: rel T
forall (a : T) (l : seq T),
(supremum l = None -> l = [::]) ->
supremum (a :: l) = None -> a :: l = [::]
    move => a l IH.
T: eqType
R: rel T
a: T
l: seq T
IH: supremum l = None -> l = [::]
supremum (a :: l) = None -> a :: l = [::]
    rewrite supremum_unfold /choose_superior.
T: eqType
R: rel T
a: T
l: seq T
IH: supremum l = None -> l = [::]
match supremum l with
| Some y => if R a y then Some a else Some y
| None => Some a
end = None -> a :: l = [::]
    by destruct (supremum l); try destruct (R a s).
  Qed.

  (** Next, we observe that the value found by [supremum] comes indeed from the
      list that it was given. *)
  Lemma supremum_in:
    forall x s,
      supremum s = Some x ->
      x \in s.
T: eqType
R: rel T
forall (x : T) (s : seq T),
supremum s = Some x -> x \in s
  Proof.
T: eqType
R: rel T
forall (x : T) (s : seq T),
supremum s = Some x -> x \in s
    move=> x.
T: eqType
R: rel T
x: T
forall s : seq T, supremum s = Some x -> x \in s
    elim => // a l IN_TAIL IN.
T: eqType
R: rel T
x, a: T
l: seq T
IN_TAIL: supremum l = Some x -> x \in l
IN: supremum (a :: l) = Some x
x \in a :: l
    rewrite in_cons; apply /orP.
T: eqType
R: rel T
x, a: T
l: seq T
IN_TAIL: supremum l = Some x -> x \in l
IN: supremum (a :: l) = Some x
x == a \/ x \in l
    move: IN; rewrite supremum_unfold.
T: eqType
R: rel T
x, a: T
l: seq T
IN_TAIL: supremum l = Some x -> x \in l
choose_superior a (supremum l) = Some x ->
x == a \/ x \in l
    destruct (supremum l); rewrite /choose_superior.
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
(if R a s then Some a else Some s) = Some x ->
x == a \/ x \in l
T: eqType
R: rel T
x, a: T
l: seq T
IN_TAIL: None = Some x -> x \in l
Some a = Some x -> x == a \/ x \in l
    {
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
(if R a s then Some a else Some s) = Some x ->
x == a \/ x \in l elim: (R a s) => EQ.
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
EQ: Some a = Some x
x == a \/ x \in l
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
EQ: Some s = Some x
x == a \/ x \in l
      -
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
EQ: Some a = Some x
x == a \/ x \in l
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
EQ: Some s = Some x
x == a \/ x \in l left; apply /eqP.
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
EQ: Some a = Some x
x = a
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
EQ: Some s = Some x
x == a \/ x \in l
        by injection EQ.
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
EQ: Some s = Some x
x == a \/ x \in l
      -
T: eqType
R: rel T
x, a: T
l: seq T
s: T
IN_TAIL: Some s = Some x -> x \in l
EQ: Some s = Some x
x == a \/ x \in l right; by apply IN_TAIL. }
T: eqType
R: rel T
x, a: T
l: seq T
IN_TAIL: None = Some x -> x \in l
Some a = Some x -> x == a \/ x \in l
    {
T: eqType
R: rel T
x, a: T
l: seq T
IN_TAIL: None = Some x -> x \in l
Some a = Some x -> x == a \/ x \in l left.
T: eqType
R: rel T
x, a: T
l: seq T
IN_TAIL: None = Some x -> x \in l
IN: Some a = Some x
x == a apply /eqP.
T: eqType
R: rel T
x, a: T
l: seq T
IN_TAIL: None = Some x -> x \in l
IN: Some a = Some x
x = a
      by injection IN. }
  Qed.

  (** To prove that [supremum] indeed computes the given sequence's supremum,
      we need to make additional assumptions on [R]. *)

  (** (1) [R] is reflexive. *)
  Hypothesis H_R_reflexive: reflexive R.
  (** (2) [R] is total. *)
  Hypothesis H_R_total: total R.
  (** (3) [R] is transitive. *)
  Hypothesis H_R_transitive: transitive R.

  (** Based on these assumptions, we show that the function [supremum] indeed
      computes an upper bound on all elements in the given sequence. *)
  Lemma supremum_spec:
    forall x s,
      supremum s = Some x ->
      forall y,
        y \in s -> R x y.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
forall (x : T) (s : seq T),
supremum s = Some x -> forall y : T, y \in s -> R x y
  Proof.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
forall (x : T) (s : seq T),
supremum s = Some x -> forall y : T, y \in s -> R x y
    move=> x s SOME_x.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
x: T
s: seq T
SOME_x: supremum s = Some x
forall y : T, y \in s -> R x y
    move: x SOME_x (supremum_in _ _ SOME_x).
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s: seq T
forall x : T,
supremum s = Some x ->
x \in s -> forall y : T, y \in s -> R x y
    elim: s; first by done.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
forall (a : T) (l : seq T),
(forall x : T,
 supremum l = Some x ->
 x \in l -> forall y : T, y \in l -> R x y) ->
forall x : T,
supremum (a :: l) = Some x ->
x \in a :: l -> forall y : T, y \in a :: l -> R x y
    move=> s1 sn IH z SOME_z IN_z_s y.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
IH: forall x : T,
supremum sn = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
SOME_z: supremum (s1 :: sn) = Some z
IN_z_s: z \in s1 :: sn
y: T
y \in s1 :: sn -> R z y
    move: SOME_z.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
IH: forall x : T,
supremum sn = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
supremum (s1 :: sn) = Some z ->
y \in s1 :: sn -> R z y rewrite supremum_unfold /choose_superior => SOME_z.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
IH: forall x : T,
supremum sn = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: match supremum sn with
| Some y =>
    if R s1 y then Some s1 else Some y
| None => Some s1
end = Some z
y \in s1 :: sn -> R z y
    destruct (supremum sn) as [b|] eqn:SUPR; last first.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
SUPR: supremum sn = None
IH: forall x : T,
None = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: Some s1 = Some z
y \in s1 :: sn -> R z y
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
y \in s1 :: sn -> R z y
    {
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
SUPR: supremum sn = None
IH: forall x : T,
None = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: Some s1 = Some z
y \in s1 :: sn -> R z y apply supremum_none in SUPR; subst.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
IH: forall x : T,
None = Some x ->
x \in [::] -> forall y : T, y \in [::] -> R x y
z: T
IN_z_s: z \in [:: s1]
y: T
SOME_z: Some s1 = Some z
y \in [:: s1] -> R z y
      rewrite mem_seq1 => /eqP ->.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
IH: forall x : T,
None = Some x ->
x \in [::] -> forall y : T, y \in [::] -> R x y
z: T
IN_z_s: z \in [:: s1]
y: T
SOME_z: Some s1 = Some z
R z s1
      by injection SOME_z => ->. }
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
y \in s1 :: sn -> R z y
    {
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
y \in s1 :: sn -> R z y rewrite in_cons => /orP [/eqP EQy | INy]; last first.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
INy: y \in sn
R z y
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
R z y
      -
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
INy: y \in sn
R z y
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
R z y have R_by: R b y
          by apply IH => //; apply supremum_in.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
INy: y \in sn
R_by: R b y
R z y
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
R z y
        apply H_R_transitive  with (y := b) => //.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
INy: y \in sn
R_by: R b y
R z b
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
R z y
        destruct (R s1 b) eqn:R_s1b;
          by injection SOME_z => <-.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
R z y
      -
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z: T
IN_z_s: z \in s1 :: sn
y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
R z y move: IN_z_s; rewrite in_cons => /orP [/eqP EQz | INz];
          first by subst.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R z y
        move: (H_R_total s1 b) => /orP [R_s1b|R_bs1].
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R_s1b: R s1 b
R z y
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R_bs1: R b s1
R z y
        +
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R_s1b: R s1 b
R z y
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R_bs1: R b s1
R z y move: SOME_z.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
EQy: y = s1
INz: z \in sn
R_s1b: R s1 b
(if R s1 b then Some s1 else Some b) = Some z -> R z y
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R_bs1: R b s1
R z y rewrite R_s1b => SOME_z.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
EQy: y = s1
INz: z \in sn
R_s1b: R s1 b
SOME_z: Some s1 = Some z
R z y
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R_bs1: R b s1
R z y
          by injection SOME_z => EQ; subst.
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R_bs1: R b s1
R z y
        +
T: eqType
R: rel T
H_R_reflexive: reflexive (T:=T) R
H_R_total: total (T:=T) R
H_R_transitive: transitive (T:=T) R
s1: T
sn: seq T
b: T
SUPR: supremum sn = Some b
IH: forall x : T,
Some b = Some x ->
x \in sn -> forall y : T, y \in sn -> R x y
z, y: T
SOME_z: (if R s1 b then Some s1 else Some b) = Some z
EQy: y = s1
INz: z \in sn
R_bs1: R b s1
R z y by destruct (R s1 b); injection SOME_z => EQ; subst. }
  Qed.

End SelectSupremum.