proposition: Lemma PC_Zero : H'_ E0zero <<= H'_ (E0_succ E0zero).
proof: Proof. intro n; destruct n; rewrite H'_eq1, H'_eq2_0; auto with arith. rewrite E0_pred_of_Succ, H'_eq1; auto with arith. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)