From Coq Require Import Arith Compare_dec Lia
     Relation_Operators RelationClasses.
From hydras Require Import Comparable Simple_LexProd ON_Generic.

Import Relations.
Generalizable All Variables.
Coercion is_true: bool >-> Sortclass.

Section Defs.

  Context `(ltA: relation A)
          (cmpA : Compare A)
          (NA: ON ltA cmpA)
          `(ltB : relation B)
          (cmpB : Compare B)
          (NB: ON ltB cmpB).

  Definition t := (B × A)%type.
  Definition lt : relation t := lexico ltB ltA.
  Definition le := clos_refl _ lt.

  #[global] Instance compare_mult : Compare t :=
    fun (alpha beta: t) ⇒
    match compare (fst alpha) (fst beta) with
    | Eq ⇒ compare (snd alpha) (snd beta)
    | c ⇒ c
    end.

  #[local] Hint Constructors clos_refl lexico: core.
  #[local] Hint Unfold lt le : core.

  Instance lt_strorder : StrictOrder lt.

  Lemma lt_wf : well_founded lt.

  Lemma compare_reflect alpha beta :
    match (compare alpha beta)
    with
      Lt ⇒ lt alpha beta
    | Eq ⇒ alpha = beta
    | Gt ⇒ lt beta alpha
    end.

  Lemma compare_correct alpha beta :
    CompSpec eq lt alpha beta (compare alpha beta).


  #[global] Instance mult_comp: Comparable lt compare_mult.

  #[global] Instance ON_mult: ON lt compare_mult.

  Lemma lt_eq_lt_dec alpha beta :
    {lt alpha beta} + {alpha = beta} + {lt beta alpha}.


End Defs.

Arguments lt_eq_lt_dec {A ltA cmpA} _ {B ltB cmpB} _.
Arguments ON_mult {A ltA cmpA} _ {B ltB cmpB}.
Arguments lt_strorder {A} {ltA} {cmpA} _ {B} {ltB} {cmpB} _.