Library hydras.OrdinalNotations.ON_Omega

A notation system for the ordinal omega Pierre Castéran, Univ. Bordeaux and LaBRI

From Coq Require Import Arith Compare_dec Lia.
From hydras Require Import ON_Generic ON_Finite.
From hydras Require Import Schutte.

Import Relations RelationClasses.

#[global]
Instance compare_nat : Compare nat := Nat.compare.

#[global] Instance Omega_comp : Comparable Peano.lt compare_nat.

#[global] Instance Omega : ON Peano.lt compare_nat.

#[local] Open Scope ON_scope.

Definition Zero_limit_succ_dec : ZeroLimitSucc_dec.
Defined.

#[global] Instance FinOrd_Omega (i:nat) :
SubON (FinOrd i) Omega i (fun alpha ⇒ proj1_sig alpha).

#[ global ] Instance omega_ok : ON_correct Schutte_basics.omega Omega finite.