proposition: Lemma sumList_summation : forall (A B : Set) f (lsa : list A)(lsb : list B), sumList lsa (fun a => sumList lsb (fun b => (f a b))) == sumList lsb (fun b => sumList lsa (fun a => (f a b))).
proof: Proof. induction lsa; destruct lsb; intuition. unfold sumList in *; simpl in *; intuition. assert (sumList (b :: lsb) (fun b : B => sumList nil (fun a : A => f a b)) == 0). eapply sumList_0. intuition. unfold sumList. simpl. intuition. rewrite H. unfold sumList in *; simpl in *; intuition. assert (sumList (a :: lsa) (fun a0 : A => sumList nil (fun b : B => f a0 b)) == 0). eapply sumList_0. intuition. unfold sumList in *; simpl in *; intuition. rewrite H. unfold sumList in *; simpl in *; intuition. rewrite sumList_body_eq. 2:{ intuition. eapply sumList_cons. } rewrite sumList_sum. rewrite (sumList_cons lsa a (fun a0 : A => sumList lsb (f a0))). rewrite IHlsa. symmetry. rewrite sumList_body_eq. 2:{ intuition. eapply sumList_cons. } rewrite sumList_sum. repeat rewrite sumList_cons. repeat rewrite <- ratAdd_assoc. eapply ratAdd_eqRat_compat; intuition. repeat rewrite ratAdd_assoc. eapply ratAdd_eqRat_compat; intuition. eapply ratAdd_comm. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation