proposition: Theorem H'_restricted_mono_l : forall beta n, Canon_plus n alpha beta -> H'_ beta n <= H'_ alpha n.
proof: Proof. now destruct (P_alpha alpha). Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)