proposition: Lemma sumList_distance_prod : forall (A : Set)(ls : list A)(f f1 f2 : A -> Rat), | (sumList ls (fun a => (f a) * (f1 a))) - (sumList ls (fun a => (f a) * (f2 a))) | <= sumList ls (fun a => (f a) * | (f1 a) - (f2 a) |).
proof: Proof. induction ls; intuition. unfold sumList; simpl in *. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. intuition. repeat rewrite sumList_cons. rewrite rat_distance_of_sum. eapply ratAdd_leRat_compat. eapply eqRat_impl_leRat. eapply ratMult_ratDistance_factor_l. eapply IHls. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation