proposition: Lemma takeUntil_step {A B} (P:Stream A → bool) `(ex:LazyExists (fun x => Is_true (P x)) s) (cons: A → B → B) (nil: B) : ¬Is_true (P s) → ∃ ex' : LazyExists (fun x => Is_true (P x)) (tl s), takeUntil P ex cons nil ≡ cons (hd s) (takeUntil P ex' cons nil).
proof: Proof. intros H. assert (ex':=ex). destruct ex' as [H0|ex']. elim H; assumption. exists (ex' tt). rewrite <- (takeUntil_wd (B:=B) (LazyFurther ex')). simpl. destruct (P s). elim H; constructor. 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