Library gaia_hydras.GHprime

From mathcomp Require Import all_ssreflect zify.
From gaia Require Export ssete9.
From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder T1 E0.
From hydras Require Paths.
From hydras Require Import Iterates Hprime L_alpha.
From gaia_hydras Require Import T1Bridge GCanon GPaths.

Set Implicit Arguments.

Definition H'_ alpha i := Hprime.H'_ (E0_g2h alpha) i.

Lemma H'_eq1 (i: nat) : H'_ E0zero i = i.

Lemma H'_eq2 alpha i :
  H'_ (E0_succ alpha) i = H'_ alpha (S i).

Lemma H'_eq3 alpha i :
  E0limit alpha → H'_ alpha i = H'_ (E0Canon alpha (S i)) i.

Lemma H'_omega k : H'_ E0_omega k = (2 × k).+1 %nat.

Lemma H'_omega_double (k: nat) :
  H'_ (E0mul E0_omega (E0fin 2)) k = (4 × k + 3)%coq_nat.

Lemma H'_dom alpha beta :
  E0lt alpha beta → dominates_strong (H'_ beta) (H'_ alpha).

Lemma H'_alpha_mono (alpha : E0) : strict_mono (H'_ alpha).

Theorem H'_alpha_gt alpha (Halpha: alpha ≠ E0zero) n :
  (n < H'_ alpha n)%N.

Lemma H'_omega_cube_min :
∀ k : nat,
  0 ≠ k → (hyper_exp2 k.+1 ≤ H'_ (E0_phi0 (E0fin 3)) k)%N.