proposition: Lemma F_mono_l: dominates (F_ alpha) (F_ beta).
proof: Proof. destruct (Lemma2_6_1_E0 H'_beta_alpha) as [i Hi]. exists (S (S i)); intros p Hp; apply F_mono_l_0 with i; auto. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)