Library hydras.Prelude.MoreOrders

From Coq Require Import RelationClasses Relation_Operators Ensembles Setoid.
Import Relation_Definitions.
Set Implicit Arguments.

Definition leq {A:Type}(lt : relation A): relation A :=
  clos_refl A lt.

Section Defs.

  Variables (A : Type)
            (lt: relation A).

  #[local] Infix "<" := lt.
  #[local] Infix "<=" := (leq lt).

  Definition Least {sto : StrictOrder lt} (x : A):=
    ∀ y, x ≤ y.

  Definition Successor {sto : StrictOrder lt} (y x : A):=
    x < y ∧ (∀ z, x < z → z < y → False).

  Definition Limit {sto : StrictOrder lt} (x:A) :=
    (∃ w:A, w < x) ∧
    (∀ y:A, y < x → ∃ z:A, y < z ∧ z < x).

  Definition Omega_limit
              {sto : StrictOrder lt} (s: nat → A) (x:A) :=
    (∀ i: nat, s i < x) ∧
    (∀ y, y < x → ∃ i:nat, y < s i).

  Definition Omega_limit_type
              `{lt : relation A}
              {sto : StrictOrder lt}
              (s: nat → A) (x:A) : Type :=
    ((∀ i: nat, s i < x) ×
     (∀ y, y < x → {i:nat | y < s i}))%type.

  Lemma Omega_limit_not_Succ
        {sto : StrictOrder lt} (s: nat → A) (x:A) :
    Omega_limit s x →
    ∀ y, ¬ Successor x y.

  Lemma Least_not_Succ {sto : StrictOrder lt} (x:A) :
    Least x → ∀ z, ¬ Successor x z.

  Lemma Omega_limit_Limit
        {sto : StrictOrder lt} (s: nat → A) (x:A) :
    Omega_limit s x → Limit x.

  Lemma Least_not_Limit {sto : StrictOrder lt} x :
    Least x → ¬ Limit x.

End Defs.

Lemma le_lt_eq {A}{lt: relation A}:
  ∀ a b, leq lt a b ↔ lt a b ∨ a = b.

#[ global ] Instance leq_trans {A:Type}{lt: relation A}{sto: StrictOrder lt}:
  Transitive (leq lt).