proposition: Lemma InfiniteSum_raw_N_cont_invariant : forall (fuel p : nat) c d (filter : Stream Q -> bool) (s : Stream Q) (q : Q), (p < 2 ^ fuel)%nat -> filter (Str_nth_tl p s) = true -> InfiniteSum_raw_N fuel filter c s q = InfiniteSum_raw_N fuel filter d s q.
proof: Proof. induction fuel. - intros. simpl in H. simpl. unfold InfiniteSum_raw_F. destruct (filter s) eqn:des. reflexivity. apply le_S_n in H. inversion H. exfalso. subst p. simpl in H0. rewrite H0 in des. discriminate. - intros. simpl. simpl in H. rewrite Nat.add_0_r in H. destruct (decide_filter_before_n (2^fuel) filter s). destruct H1 as [k [H1 H2]]. apply (IHfuel k). exact H1. exact H2. destruct (Nat.lt_ge_cases p (2^fuel)). exfalso. specialize (H1 p H2). rewrite H0 in H1. discriminate. apply Nat.le_exists_sub in H2. destruct H2 as [k [H2 _]]. subst p. rewrite <- Str_nth_tl_plus in H0. rewrite (InfiniteSum_raw_N_step fuel (fun s0 : Stream Q => InfiniteSum_raw_N fuel filter c s0)). 2: exact H1. rewrite (InfiniteSum_raw_N_step fuel (fun s0 : Stream Q => InfiniteSum_raw_N fuel filter d s0)). 2: exact H1. apply (IHfuel k). apply Nat.add_lt_mono_r in H. exact H. exact H0. 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