proposition: Theorem sumList_subset_le : forall (A : Set){eqd: EqDec A}(ls1 ls2 : list A)(f : A -> Rat), NoDup ls1 -> NoDup ls2 -> (forall a, In a ls1 -> In a ls2) -> sumList ls1 f <= sumList ls2 f.
proof: Proof. induction ls1; intuition; simpl in *. unfold sumList; simpl. eapply rat0_le_all. inversion H; clear H; subst. rewrite sumList_cons. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply (@sumList_permutation _ _ _ (a :: removeFirst (EqDec_dec _) ls2 a)%list). eapply removeFirst_permutation. eapply H1. intuition. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply sumList_cons. } eapply ratAdd_leRat_compat; intuition. eapply IHls1; intuition. eapply removeFirst_NoDup. trivial. destruct (EqDec_dec _ a a0). subst. intuition. eapply removeFirst_in. eapply H1; intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation