proposition: Lemma L04' : forall beta, E0limit beta -> forall n, (S n) o<= (Canon.Canon beta (S n)).
proof: Proof. destruct beta; unfold E0limit. cbn; intros; rewrite Le_iff; split. - apply (@E0.cnf_ok (E0finS n0)). - cbn; split. + apply L04; auto. + cbn; apply Canon.nf_canon; auto. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)