proposition: Lemma HFLim : E0limit alpha -> P alpha.
proof: Proof. intros Halpha n; rewrite H'_eq3. - rewrite CanonS_phi0_lim; [| trivial]. rewrite F_lim_eqn; auto. + transitivity (H'_ (E0_phi0 (Canon alpha (S n))) (S n)). * apply IHalpha. apply CanonS_lt. now apply Limit_not_Zero. * apply H'_restricted_mono_l. red; cbn; apply KS_thm_2_4_lemma5. -- apply Cor12_1 with 0. ++ apply nf_canon, cnf_ok. ++ apply canonS_limit_mono. ** apply cnf_ok. ** destruct alpha; cbn; assumption. ** auto with arith. ++ auto with arith. ++ apply KS_thm_2_4. ** apply cnf_ok. ** destruct alpha; auto. ** auto with arith. -- apply nf_canon, cnf_ok. -- apply T1limit_canonS_not_zero. ++ apply cnf_ok. ++ now destruct alpha. - apply T1limit_phi0. apply Limit_not_Zero; auto. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)