proposition: Lemma Σ_Qball (f g: nat -> Q) (e: Q) (n: nat): 0 <= e -> (forall i: nat, (i < n)%nat -> Qabs (f i - g i) <= e / inject_Z (Z.of_nat n)) -> Qball e (Σ n f) (Σ n g).
proof: Proof. Proof with auto. intros epos H. apply Qball_Qabs. destruct n. simpl. exact epos. rewrite Σ_sub. setoid_replace e with (inject_Z (Z.of_nat (S n)) * (/ inject_Z (Z.of_nat (S n)) * e)). apply Σ_abs_le. intros ? E. specialize (H x E). rewrite Qmult_comm. assumption. unfold canonical_names.equiv, stdlib_rationals.Q_eq. field. discriminate. Qed.
imports: CoRN.stdlib_omissions.List Coq.QArith.QArith Coq.QArith.Qabs CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric Coq.Program.Program CoRN.stdlib_omissions.N CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q