proposition: Remark RC : H'_ alpha <<= H'_ (E0_succ alpha).
proof: Proof. subst alpha; intro n; repeat rewrite H'_eq2. destruct (Halpha beta). - apply Lt_Succ. - specialize (PA0 (S n) (S (S n))); abstract lia. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)