proposition: Lemma L_ok_lim alpha : (forall beta, (beta o< alpha)%e0 -> P beta) -> E0limit alpha -> P alpha.
proof: Proof. Proof with eauto with E0. unfold P; intros. apply L_spec_compat with (fun k => L_ (Canon alpha k) (S k)). - generalize L_lim_ok; intro H1; unfold L_lim in H1. assert (H2 : T1limit (cnf alpha)) by (now destruct alpha). specialize (H1 (cnf alpha) cnf_ok H2 (fun k i => L_ (Canon alpha k) i)). apply H1; intro k; specialize (H (Canon alpha (S k))). assert (H3: (Canon alpha (S k) o< alpha)%e0 ). { apply CanonS_lt; now apply Limit_not_Zero. } apply H in H3; apply L_spec_compat with (L_ (Canon alpha (S k))); auto. - intro n; rewrite (L_lim_eqn alpha); trivial. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)