proposition: Lemma H'_alpha_mono_weak : forall k l, k <= l -> H'_ alpha k <= H'_ alpha l.
proof: Proof. intros. destruct (Compat815.le_lt_or_eq k l H). - now apply Nat.lt_le_incl, H'_alpha_mono. - subst; auto. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)