proposition: Lemma F_One_Zero_dom : dominates_from 1 (F_ 1) (F_ E0zero).
proof: Proof. red;intros. rewrite F_zero_eqn. rewrite LF1; abstract lia. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)