proposition: Lemma sumList_le : forall (A : Set)(ls : list A)(f1 f2 : A -> Rat), (forall a, In a ls -> f1 a <= f2 a) -> sumList ls f1 <= sumList ls f2.
proof: Proof. induction ls; intuition. unfold sumList; simpl in *. intuition. rewrite sumList_cons. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite sumList_cons. eapply eqRat_refl. } simpl in *. eapply ratAdd_leRat_compat. eapply H. intuition. eapply IHls. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation