proposition: Theorem H'_dom : dominates_strong (H'_ beta) (H'_ alpha).
proof: Proof. destruct H'_mono_l as [x Hx]; exists (S x); red. intros p H; inversion_clear H; apply Hx; auto with arith. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)