proposition: Lemma Σ_Qball_pos_bounds (f g: nat -> Q) (e: Q) (n: positive): (forall i: nat, (i < Pos.to_nat n)%nat -> Qball (e * (1#n)) (f i) (g i)) -> Qball e (Σ (Pos.to_nat n) f) (Σ (Pos.to_nat n) g).
proof: Proof. Proof with intuition. intros. assert (0 <= e). { specialize (H O (Pos2Nat.is_pos n)). apply (msp_nonneg (msp (Q_as_MetricSpace))) in H. rewrite <- (Qmult_0_l (1#n)) in H. apply Qmult_le_r in H. exact H. reflexivity. } apply Σ_Qball. exact H0. intros. setoid_replace (e / inject_Z (Z.of_nat (nat_of_P n))) with (e * (1#n)). apply Qball_Qabs... unfold canonical_names.equiv, stdlib_rationals.Q_eq. rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P... 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