proposition: Fact F2 : forall i, (1 <= i -> F_ beta i < F_ alpha i)%nat.
proof: Proof. subst alpha; intros i H; apply (F_alpha_dom beta i H). Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)