proposition: Remark R3 : {n: nat | forall p, n <= p -> H'_ alpha (S p) < H'_ beta (S p)}.
proof: Proof. destruct R2 as [n Hn]; exists (Nat.max n 1). intros p H; apply Nat.le_lt_trans with (H'_ gamma (S p)). - apply Hn; lia. - subst beta; apply (H'_alpha_dom gamma (S p)); auto with arith. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)