proposition: Lemma H'_eq1 : forall i, H'_ E0zero i = i.
proof: Proof. intro i; now rewrite H'__equation_1. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)