Section relations.

  Require Export Relations.
  Require Export Arith.
  Variable Alpha : Set.
  Variable r : relation Alpha.
  Definition binop := Alpha → Alpha → Alpha.
  Variable (sup : binop).
  Definition lub :=
    (∀ a b : Alpha, r a (sup a b)) ∧
    (∀ a b : Alpha, r b (sup a b)) ∧
    (∀ a b c : Alpha, r a c ∧ r b c → r (sup a b) c).

  Definition inv (R : relation Alpha) : relation Alpha := fun a b ⇒ R b a.

  Definition strict (R : relation Alpha) : relation Alpha :=
    fun a b ⇒ R a b ∧ a ≠ b.

  Definition ascending_chain := well_founded (strict (inv r)).

  Inductive nondep_lexprod (A1 A2 : Set) (ra : relation A1)
    (rb : relation A2) : relation (A1 × A2) :=
    | lexprod_inf :
      ∀ a1 a2 : A1,
        ra a1 a2 →
        ∀ b1 b2 : A2, nondep_lexprod A1 A2 ra rb (a1, b1) (a2, b2)
    | lexprod_eq :
      ∀ b1 b2 : A2,
        rb b1 b2 → ∀ a : A1, nondep_lexprod A1 A2 ra rb (a, b1) (a, b2).

End relations.

Implicit Arguments strict [Alpha].
Implicit Arguments inv [Alpha].
Implicit Arguments ascending_chain [Alpha].