proposition: Lemma fold_add_iter_le : forall (A : Set)(ls : list A) f r init, fold_left (fun r a => r + (f a)) ls init <= r -> init <= r /\ (forall a, In a ls -> f a <= r).
proof: Proof. induction ls; intuition; simpl in *; intuition; subst. assert (init + f a <= r). eapply IHls. apply H. eapply ratAdd_any_le; eauto. assert (init + f a0 <= r). eapply IHls. eauto. eapply ratAdd_any_le. eapply leRat_trans. apply eqRat_impl_leRat. apply ratAdd_comm. eauto. edestruct IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool