proposition: Lemma Qball_hetero_Σ (n m: positive) f g (e:Q): (forall i: nat, (i < Pos.to_nat (n * m)%positive)%nat -> Qball (e * (1# (n * m)%positive)) (/ inject_Z (Zpos m) * f (i / Pos.to_nat m)%nat) (/ inject_Z (Zpos n) * g (i / Pos.to_nat n)%nat)) -> Qball e (Σ (Pos.to_nat n) f) (Σ (Pos.to_nat m) g).
proof: Proof. intros. rewrite (Σ_multiply_bound (Pos.to_nat n) m). rewrite (Σ_multiply_bound (nat_of_P m) n). rewrite Nat.mul_comm. rewrite <- nat_of_P_mult_morphism. unfold Qdiv. rewrite Σ_mult. rewrite Σ_mult. apply Σ_Qball_pos_bounds. intros. unfold Basics.compose. unfold flip. 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