proposition: Lemma Lt_n_F_Zero_n : forall n:nat, n < F_ E0zero n.
proof: Proof. intros n ; rewrite F_zero_eqn; auto with arith. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)