fact: Record P (alpha:E0) : Prop := mkP { PA : strict_mono (F_ alpha); PB : forall n, n < F_ alpha n; PC : F_ alpha <<= F_ (E0_succ alpha); PD : dominates_from 1 (F_ (E0_succ alpha)) (F_ alpha); PE : forall beta n, Canon_plus n alpha beta -> F_ beta n <= F_ alpha n}.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)