proposition: Remark RB : alpha <> E0zero ->forall n, (n < H'_ alpha n)%nat.
proof: Proof. intros _ n; subst alpha; rewrite H'_eq2; destruct (E0_eq_dec beta E0zero). - subst; rewrite H'_eq1; auto with arith. - destruct (Halpha beta). + apply Lt_Succ. + transitivity (S n); auto with arith. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)