proposition: Lemma LF2_0 : dominates_from 0 (F_ 2) (fun i => exp2 i * i).
proof: Proof. red. intros ; apply LF2 ; auto. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)