proposition: Lemma takeUntil_length_correct {A} (P : Stream A → bool) `(ex : !LazyExists (fun x => Is_true (P x)) s) : Is_true (P (Str_nth_tl (takeUntil_length P ex) s)).
proof: Proof. assert (ex':=ex). unfold takeUntil_length. induction ex' as [s|s ? IH]. now rewrite takeUntil_end. case_eq (P s); intros E. rewrite takeUntil_end; auto with *. destruct (takeUntil_step P ex (λ _ : A, S) O) as [ex1 E1]. now apply Is_true_neq_left. rewrite E1. now apply (IH tt). 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