proposition: Lemma H'_mono_l : {n: nat | forall p, n <= p -> H'_ alpha (S p) < H'_ beta (S p)}.
proof: Proof. destruct (Zero_Limit_Succ_dec beta) as [[H0 | Hl] | [gamma Hgamma]]. - subst; destruct (E0_not_Lt_zero H_alpha_beta). - now apply R5. - eapply R3; eauto. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)