Library gaia_hydras.ON_gfinite
ordinals a la mathcomp
From hydras Require Import DecPreOrder ON_Generic.
From mathcomp Require Import all_ssreflect zify.
From gaia Require Export ssete9.
From Coq Require Import Logic.Eqdep_dec.
Set Implicit Arguments.
Definition finord_lt (n:nat) (alpha beta: 'I_n): bool :=
(alpha < beta)%N.
#[global] Instance finord_compare (n:nat) : Compare ('I_n) :=
fun alpha beta ⇒ Nat.compare alpha beta.
Lemma finord_compare_correct (n:nat) (alpha beta : 'I_n) :
CompSpec eq (@finord_lt n) alpha beta (compare alpha beta).
#[global] Instance finord_sto n : StrictOrder (@finord_lt n).
#[global] Instance finord_comp n :
Comparable (@finord_lt n) (@finord_compare n).
Lemma finord_lt_wf n : well_founded (@finord_lt n).
#[global] Instance finord_ON n : ON (@finord_lt n) (@finord_compare n).
From mathcomp Require Import all_ssreflect zify.
From gaia Require Export ssete9.
From Coq Require Import Logic.Eqdep_dec.
Set Implicit Arguments.
Definition finord_lt (n:nat) (alpha beta: 'I_n): bool :=
(alpha < beta)%N.
#[global] Instance finord_compare (n:nat) : Compare ('I_n) :=
fun alpha beta ⇒ Nat.compare alpha beta.
Lemma finord_compare_correct (n:nat) (alpha beta : 'I_n) :
CompSpec eq (@finord_lt n) alpha beta (compare alpha beta).
#[global] Instance finord_sto n : StrictOrder (@finord_lt n).
#[global] Instance finord_comp n :
Comparable (@finord_lt n) (@finord_compare n).
Lemma finord_lt_wf n : well_founded (@finord_lt n).
#[global] Instance finord_ON n : ON (@finord_lt n) (@finord_compare n).
Examples
#[program] Example o_33_of_42: 'I_42 := @Ordinal 42 33 _.
#[program] Example o_36_of_42: 'I_42 := @Ordinal 42 36 _.