proposition: Lemma sumList_rel_distance : forall (A : Set)(ls : list A)(f1 f2 : A -> Rat -> Prop) r r1 r2, (forall a r1 r2, In a ls -> f1 a r1 -> f2 a r2 -> (ratDistance r1 r2) <= r) -> sumList_rel f1 ls r1 -> sumList_rel f2 ls r2 -> ratDistance r1 r2 <= (r * (length ls / 1)).
proof: Proof. induction ls; intuition; simpl in *. inversion H0. inversion H1. subst. rewrite H2. rewrite H3. eapply leRat_trans. eapply eqRat_impl_leRat. eapply (ratIdentityIndiscernables 0). intuition. eapply rat0_le_all. inversion H0; clear H0; subst. inversion H1; clear H1; subst. rewrite ratS_num. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply eqRat_symm. eapply ratMult_distrib. } rewrite H7. rewrite H9. rewrite rat_distance_of_sum. eapply ratAdd_leRat_compat. rewrite <- ratMult_1_r. eapply ratMult_leRat_compat. eapply H; eauto. intuition. eapply IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation