proposition: Lemma AltSeries_wd : forall (X Y:Type) (f : X*Q -> X*Q) (g : Y*Q -> Y*Q) (x : X*Q) (y : Y*Q) cvmod ccvmod (fdecr : Str_alt_decr X f x) (gdecr : Str_alt_decr Y g y) (flz : Limit_zero X f x cvmod) (glz : Limit_zero Y g y ccvmod), (forall p:positive, Str_pth _ f p x == Str_pth _ g p y) -> (forall e, cvmod e ≡ ccvmod e) -> (AltSeries X f x cvmod fdecr flz == AltSeries Y g y ccvmod gdecr glz)%CR.
proof: Proof. intros. apply regFunEq_equiv, regFunEq_e. intros e. simpl. setoid_replace (SumStream X f x (cvmod e) e) with (SumStream Y g y (cvmod e) e). rewrite H0. apply ball_refl. apply (Qpos_nonneg (e+e)). unfold SumStream. destruct (iterate_stop_correct _ (fun y0 : X * Q * Q => let (z, r) := f (fst y0) in (z, r, Qred (r + snd y0))) (fun y0 : X * Q * Q => Qle_bool (Qabs (snd (fst y0))) (` e)) (cvmod e) (x,0)) as [q [qeq [H1 H2]]]. rewrite qeq, SumStream_red. clear qeq. destruct (iterate_stop_correct _ (fun y0 : Y * Q * Q => let (z, r) := g (fst y0) in (z, r, Qred (r + snd y0))) (fun y0 : Y * Q * Q => Qle_bool (Qabs (snd (fst y0))) (` e)) (cvmod e) (y,0)) as [r [req [H3 H4]]]. rewrite req, SumStream_red. clear req. destruct H4 as [fuel|predicate]. - subst r. destruct H2. + subst q. apply (SumStream_wd _ _ _ _ _ _ _ H). + exfalso. destruct H2. specialize (H3 q H2). rewrite SumStream_fst_red in H3. unfold fst in H3. rewrite SumStream_fst_red in H4. unfold fst in H4. specialize (H q). unfold Str_pth in H. rewrite H in H4. rewrite H4 in H3. discriminate. - destruct predicate. rewrite SumStream_fst_red in H5. unfold fst in H5. destruct H2. + exfalso. subst q. specialize (H1 r H4). rewrite SumStream_fst_red in H1. unfold fst in H1. specialize (H r). unfold Str_pth in H. rewrite <- H in H5. rewrite H5 in H1. discriminate. + destruct H2. rewrite SumStream_fst_red in H6. unfold fst in H6. destruct (Pos.lt_total q r). exfalso. specialize (H3 q H7). rewrite SumStream_fst_red in H3; unfold fst in H3. specialize (H q). unfold Str_pth in H. rewrite H in H6. rewrite H6 in H3. discriminate. destruct H7. rewrite H7. exact (SumStream_wd _ _ _ _ _ _ _ H). exfalso. specialize (H1 r H7). rewrite SumStream_fst_red in H1; unfold fst in H1. specialize (H r). unfold Str_pth in H. rewrite H in H1. rewrite H1 in H5. discriminate. Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra