proposition: Lemma fastΣ_correct n f: fastΣ n f == Σ n f.
proof: Proof. intros. rewrite <- (Qplus_0_r (Σ n f)). unfold Σ, fastΣ. generalize 0. induction n; intros. simpl. ring. change (fast f n (Qred (q + f n)) == Qsum (map f (enum (S n))) + q). rewrite IHn. rewrite Qred_correct. simpl. ring. 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