proposition: Lemma sumList_sum : forall (A : Set)(ls : list A)(f1 f2 : A -> Rat), sumList ls (fun a => f1 a + f2 a) == sumList ls f1 + sumList ls f2.
proof: Proof. induction ls; intuition; unfold sumList in *; simpl in *. rewrite <- ratAdd_0_l. intuition. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } rewrite fold_add_init. rewrite (IHls f1 f2). eapply eqRat_trans. 2:{ symmetry. eapply ratAdd_eqRat_compat. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } eapply fold_add_init. intuition. eapply eqRat_refl. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } eapply fold_add_init. intuition. eapply eqRat_refl. } repeat rewrite <- ratAdd_assoc. eapply ratAdd_eqRat_compat. repeat rewrite ratAdd_assoc. eapply ratAdd_eqRat_compat; intuition. rewrite ratAdd_comm. eapply ratAdd_eqRat_compat; intuition. eapply fold_add_body_eq; intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation