proposition: Lemma H'_mono_l_0 alpha beta : alpha o< beta -> {n : nat | forall p, n <= p -> H'_ alpha (S p) <= H'_ beta (S p)}.
proof: Proof. intro H; destruct (Lemma2_6_1_E0 H) as [n Hn]. exists (S n). intros; apply H'_restricted_mono_l. eapply Cor12_E0 with n; eauto. lia. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)