proposition: Theorem sumList_ne_0 : forall (ls : list A)(f : A -> Rat), ~ (sumList ls f) == 0 -> exists b : _, In b ls /\ ~ ((f b) == 0).
proof: Proof. Abort. Theorem sumList_perm : forall (ls1 ls2 : list A)(f1 f2 : A -> Rat), Permutation ls1 ls2 -> (forall b, (f1 b) == (f2 b)) -> (sumList ls1 f1) == (sumList ls2 f2). Abort. Lemma fold_add_init : forall (ls : list A)(f : A -> Rat) init1 init2, fold_left (fun (r : Rat) (a : A) => r + (f a)) ls (init1 + init2) == init1 + (fold_left (fun (r : Rat) (a : A) => r + (f a)) ls init2). induction ls; intuition; simpl in *. eapply eqRat_refl. eapply eqRat_trans. eapply IHls. eapply eqRat_trans. eapply ratAdd_assoc. eapply ratAdd_eqRat_compat. eapply eqRat_refl. eapply eqRat_symm. eapply IHls. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool