proposition: Lemma sumList_rel_le : forall (A : Set)(ls : list A)(f1 f2 : A -> Rat -> Prop) r1 r2, sumList_rel f1 ls r1 -> sumList_rel f2 ls r2 -> (forall a v1 v2, In a ls -> f1 a v1 -> f2 a v2 -> v1 <= v2) -> r1 <= r2.
proof: Proof. induction ls; intuition. inversion H; clear H; subst. rewrite H2. eapply rat0_le_all. inversion H; clear H; subst. inversion H0; clear H0; subst. rewrite H7. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply H9. } eapply ratAdd_leRat_compat. eapply H1. simpl. left. eauto. trivial. trivial. eapply IHls. eauto. eauto. intuition. eapply H1. simpl. right. eauto. trivial. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation