proposition: Lemma decide_filter_before_n : forall (n : nat) (filter : Stream Q -> bool) (s : Stream Q), (exists p:nat, lt p n /\ filter (Str_nth_tl p s) = true) \/ (forall p:nat, lt p n -> filter (Str_nth_tl p s) = false).
proof: Proof. induction n. - intros. right. intros. exfalso. inversion H. - intros. destruct (filter (Str_nth_tl n s)) eqn:des. left. exists n. split. apply Nat.le_refl. exact des. destruct (IHn filter s). + left. destruct H as [p [H H0]]. exists p. split. apply le_S, H. exact H0. + right. intros. apply Nat.le_succ_r in H0. destruct H0. apply H, H0. inversion H0. subst p. exact des. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qpower Coq.QArith.Qabs Coq.ZArith.Zdiv