proposition: Fact F7 : forall i, (S n < i -> F_ (E0_succ beta) i <= F_ alpha i)%nat.
proof: Proof. intros; apply F_restricted_mono_l; apply F6; auto. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)