proposition: Lemma Σ_multiply_bound (n:nat) (k: positive) (f: nat -> Q): Σ n f == Σ (Pos.to_nat k * n) (f ∘ flip Nat.div (Pos.to_nat k)) / inject_Z (Zpos k).
proof: Proof. rewrite <- Qmult_Σ. rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P. 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