proposition: Remark RBlim : forall n, (n < H'_ alpha n)%nat.
proof: Proof. intro n; rewrite H'_eq3; auto. destruct (Halpha (Canon alpha (S n))). - apply Canon_lt; now apply Limit_not_Zero. - eapply PB0; intro H. assert (H0 :cnf (Canon alpha (S n)) = cnf E0zero) by (f_equal; auto). simpl in H0; apply (@T1limit_canonS_not_zero n (cnf alpha)); auto. + apply cnf_ok. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)