proposition: Lemma PD_Zero : dominates_from 1 (H'_ (E0_succ E0zero)) (H'_ E0zero).
proof: Proof. red;intros; rewrite H'_eq1, H'_eq2_0, E0_pred_of_Succ, H'_eq1. - abstract lia. - apply Succ_Succb. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)