proposition: Remark R2 : {n : nat | forall p, n <= p -> H'_ alpha (S p) <= H'_ gamma (S p)}.
proof: Proof. apply H'_mono_l_1, R1. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)