proposition: Lemma PA_Zero : strict_mono (H'_ E0zero).
proof: Proof. intros n p H; repeat rewrite H'_eq1; auto with arith. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)