proposition: Lemma InfiniteGeometricSum_raw_correct : forall (series : Stream Q) (e : QposInf), GeometricSeries series -> InfiniteGeometricSum_raw series e = InfiniteGeometricSum_fat series e.
proof: Proof. assert (forall n:nat, lt 0 n -> Pos.of_nat (2 ^ n) = (2 ^ Pos.of_nat n)%positive) as inj_pow. { induction n. - intros. exfalso; inversion H. - intros _. destruct n. reflexivity. rewrite Nat2Pos.inj_succ. 2: discriminate. rewrite Pos.pow_succ_r. rewrite <- IHn. 2: apply le_n_S, Nat.le_0_l. clear IHn. generalize (S n). intro k. change (2 ^ S k)%nat with (2 * 2 ^ k)%nat. rewrite Nat2Pos.inj_mul. reflexivity. discriminate. apply Nat.pow_nonzero. discriminate. } intros. destruct e. 2: reflexivity. simpl. rewrite InfiniteSum_raw_N_correct. apply InfiniteSum_fat_add_stop. 2: apply InfiniteGeometricSum_maxIter_correct, H. specialize (inj_pow (Pos.to_nat (Pos.size (InfiniteGeometricSum_maxIter series q))) (Pos2Nat.is_pos _)). rewrite Pos2Nat.id in inj_pow. rewrite <- Nat2Pos.id. rewrite inj_pow. apply Pos2Nat.inj_le. apply Pos.lt_le_incl, Pos.size_gt. apply Nat.pow_nonzero. discriminate. 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