Library hydras.OrdinalNotations.Example_3PlusOmega

From hydras Require Import ON_plus ON_Finite ON_Omega.
Import ON_Generic.
From Coq Require Import Compare_dec Lia Logic.Eqdep_dec.

Definition O3O := ON_plus (FinOrd 3) Omega.
#[ global ] Existing Instance O3O.

Arguments ON_t : clear implicits.
Arguments ON_t {A lt cmp} _.

Program Definition f (z: ON_t O3O) : ON_t Omega :=
  match z with inl i ⇒ i | inr j ⇒ 3+j end.

Program Definition g (a : ON_t Omega) : ON_t O3O :=
  match (le_lt_dec 3 a) with
    left _ ⇒ inr (a - 3)
  | right _ ⇒ inl a
  end.

#[ global ] Instance L_3_plus_omega : ON_Iso _ _ f g.