fact: Fixpoint takeUntil {A B : Type} (P : Stream A → bool) {s : Stream A} (ex:LazyExists (fun x => Is_true (P x)) s) (cons: A → B → B) (nil : B) : B := (if P s as b return ((Is_true (P s) → Is_true b) → B) then λ _, nil else λ (n : Is_true (P s) → False), cons (hd s) (@takeUntil A B P (tl s) match ex with | LazyHere H => (False_ind _ (n H)) | LazyFurther ex0 => ex0 tt end cons nil)) (λ x, x).
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