proposition: Lemma Qmult_Σ (f: nat -> Q) n (k: nat): Σ n f * inject_Z (Z.of_nat k) == Σ (k * n) (f ∘ flip Nat.div k).
proof: Proof. Proof with auto with *. unfold Basics.compose. rewrite Nat.mul_comm. rewrite Σ_mult_bound. unfold Qdiv. rewrite Σ_mult. apply Σ_wd. intros. unfold Basics.compose. rewrite (Σ_constant (f x))... intros. unfold flip. replace ((x * k + i) / k)%nat with x... apply (Nat.div_unique (x * k + i)%nat k x i)... 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