proposition: Lemma L_lim_ok : L_spec lambda L_lim.
proof: Proof. right. - apply T1limit_not_zero; auto. - intro k; unfold L_lim. red; path_decompose (S k). instantiate (1:= canon lambda (S k)). * specialize (H k); inversion H. -- generalize (canon_not_null k); rewrite <- H0; now destruct 1. -- apply H1. * rewrite interval_singleton; left. -- discriminate. -- split. ++ apply T1limit_not_zero; auto. ++ reflexivity. * specialize (L_pos_inv (canon lambda (S k)) (f (S k)) (canon_not_null k) (H k) (S k)); abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)