From mathcomp Require Import all_ssreflect zify.
From gaia Require Export ssete9.
From Coq Require Import Logic.Eqdep_dec Arith.
From hydras Require Import DecPreOrder.
From hydras Require Import T1 E0.
From hydras Require Paths.

From hydras Require Import primRec.
From hydras Require Import F_alpha F_omega.

From gaia_hydras Require Import T1Bridge GCanon GHprime.

Set Implicit Arguments.

Notation hF_ := F_alpha.F_.

Definition F_ (alpha : E0) := F_alpha.F_ (E0_g2h alpha).

#[program]
 Definition T1F_ (a : T1)(Hnf : T1nf a == true) (n:nat) : nat:=
  (F_ (@mkE0 a _) n).

Lemma F_alpha_gt (alpha : E0) (n : nat): (n < F_ alpha n)%N.

Lemma F_alpha_mono (alpha: E0): strict_mono (F_ alpha).

Lemma F_alpha_dom alpha:
  dominates_from 1 (F_ (E0_succ alpha)) (F_ alpha).


Lemma F_alpha_Succ_le alpha:
 fun_le (F_ alpha) (F_ (E0_succ alpha)).

Lemma F_alpha_positive (alpha : hE0) (n : nat): (0 < F_alpha.F_ alpha n)%N.

Lemma F_zeroE i: F_ E0zero i = i.+1.

Lemma F_mono_l alpha beta:
  E0lt beta alpha → dominates (F_ alpha) (F_ beta).

Lemma F_alpha_0_eq (alpha : E0): F_ alpha 0 = 1.

Lemma F_succE alpha i :
  F_ (E0_succ alpha) i = Iterates.iterate (F_ alpha) i.+1 i.

Lemma F_limE alpha i:
  T1limit (cnf alpha) → F_ alpha i = F_ (E0Canon alpha i) i.

Lemma LF1 i: F_ (E0fin 1) i = ((2 × i) .+1)%N.

Lemma LF2 i: (Exp2.exp2 i × i < F_ (E0fin 2) i)%N.

Lemma LF2' i: (1 ≤ i)%N → (Exp2.exp2 i < F_ (E0fin 2) i)%N.

Lemma LF3_2:
  Iterates.dominates_from 2 (F_ (E0fin 3))
    (fun n : nat ⇒ Iterates.iterate Exp2.exp2 n.+1 n).

Definition Canon_plus n alpha beta :=
  Paths.Canon_plus n (E0_g2h alpha) (E0_g2h beta).

Lemma F_restricted_mono_l alpha beta n:
    Canon_plus n alpha beta → (F_ beta n ≤ F_ alpha n)%N.

Lemma H'_F alpha n : (F_ alpha n.+1 ≤ H'_ (E0_phi0 alpha) n.+1)%N.

Lemma F_alpha_not_PR_E0 alpha:
  E0le E0_omega alpha → isPR 1 (F_ alpha) → False.

Lemma F_alpha_not_PR alpha (Hnf: T1nf alpha == true):
  LE T1omega alpha → isPR 1 (@T1F_ alpha Hnf) → False.