proposition: Remark R5 : {n: nat | forall p, n <= p -> H'_ alpha (S p) < H'_ beta (S p)}.
proof: Proof. assert (E0_succ alpha o<= beta) by (apply Lt_Le_incl; apply R4). destruct (H'_mono_l_1 _ _ H) as [x Hx]. exists x; intros. apply Nat.lt_le_trans with (H'_ (E0_succ alpha) (S p)). - apply (H'_alpha_dom alpha (S p)); auto with arith. - auto. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)