proposition: Lemma takeUntil_end {A B} (P:Stream A → bool) `(ex:LazyExists (fun x => Is_true (P x)) seq) (cons:A → B → B) (nil : B) : Is_true (P seq) → takeUntil P ex cons nil ≡ nil.
proof: Proof. intros H. rewrite <- (takeUntil_wd (B:=B) (LazyHere (P:= (fun x => Is_true (P x))) H)). unfold takeUntil. destruct (P seq);[|contradiction]. 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