proposition: Lemma H'_mono_l_1 alpha beta : alpha o<= beta -> {n : nat | forall p, n <= p -> H'_ alpha (S p) <= H'_ beta (S p)}.
proof: Proof. intro H; destruct (le_lt_eq_dec H). - now apply H'_mono_l_0. - subst; exists 0; auto with arith. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)