proposition: Lemma takeUntil_length_tl {A} (P : Stream A → bool) `(ex : !LazyExists (fun x => Is_true (P x)) s) (Ptl : EventuallyForAll (fun x => Is_true (P x)) s) : takeUntil_length P ex ≤ S (takeUntil_length P (LazyExists_tl ex Ptl)).
proof: Proof. unfold takeUntil_length. destruct ex. rewrite takeUntil_end. now apply nat_nonneg. easy. simpl. case_eq (P s); intros E. rewrite takeUntil_end. now apply nat_nonneg. apply Ptl. auto with *. reflexivity. 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