proposition: Lemma takeUntil_length_Str_nth_tl {A} (P : Stream A → bool) `(ex : !LazyExists (fun x => Is_true (P x)) s) (Ptl : EventuallyForAll (fun x => Is_true (P x)) s) (n : nat) : takeUntil_length P ex ≤ n + takeUntil_length P (LazyExists_Str_nth_tl ex Ptl n).
proof: Proof. Proof with auto with *. revert s ex Ptl. induction n; intros. easy. transitivity (S (takeUntil_length P (LazyExists_tl ex Ptl))). apply takeUntil_length_tl. simpl. apply le_n_S. unfold takeUntil_length. setoid_rewrite (takeUntil_wd (LazyExists_Str_nth_tl ex Ptl (S n)) (LazyExists_Str_nth_tl (LazyExists_tl ex Ptl) (ForAll_Str_nth_tl 1 Ptl) n) (λ _, S) O). apply IHn. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax Coq.QArith.QArith Coq.Bool.Bool CoRN.metric2.Complete MathClasses.theory.CoqStreams MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals