proposition: Lemma sumList_cons : forall (A : Set)(ls : list A) a f, sumList (a :: ls) f == f a + (sumList ls f).
proof: Proof. intuition. unfold sumList. simpl. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } rewrite fold_add_init. eapply eqRat_refl. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation