proposition: Lemma Σ_abs_le f n (b: Q): (forall x, (x < n)%nat -> Qabs (f x) <= b) -> Qabs (Σ n f) <= inject_Z (Z.of_nat n) * b.
proof: Proof. induction n. discriminate. intros. rewrite S_Zplus. rewrite Q.Zplus_Qplus. change (Qabs (f n + Σ n f) <= (inject_Z (Z.of_nat n) + 1) * b)%Q. assert ((inject_Z (Z.of_nat n) + 1) * b == b + inject_Z (Z.of_nat n) * b)%Q. ring. rewrite H0. clear H0. apply Qle_trans with (Qabs (f n) + Qabs (Σ n f))%Q. apply Qabs_triangle. apply Qplus_le_compat; auto. 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