proposition: Lemma fold_add_comm : forall (A B : Set)(lsa : list A)(lsb : list B) f, fold_left (fun r1 a => r1 + (fold_left (fun r2 b => r2 + (f a b)) lsb 0)) lsa 0 == fold_left (fun r1 b => r1 + (fold_left (fun r2 a => r2 + (f a b)) lsa 0)) lsb 0.
proof: Proof. induction lsa; destruct lsb; intuition; simpl in *; intuition. apply eqRat_symm. eapply eqRat_trans. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_r. apply eqRat_refl. apply eqRat_refl. apply fold_add_eq_init. eapply eqRat_trans. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_r. apply eqRat_refl. apply eqRat_refl. apply fold_add_eq_init. eapply eqRat_trans. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_l. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_l. apply eqRat_refl. apply eqRat_refl. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_l. apply eqRat_refl. apply eqRat_refl. simpl. eapply eqRat_trans. eapply fold_add_body_eq; intuition. eapply eqRat_refl. eapply fold_add_init_0. simpl. eapply eqRat_trans. eapply fold_add_init_0. eapply eqRat_trans. eapply ratAdd_eqRat_compat. apply eqRat_refl. eapply eqRat_trans. eapply fold_add_body_eq; intuition. apply ratAdd_0_r. apply eqRat_refl. apply eqRat_symm. eapply fold_add_eq. eapply eqRat_trans. eapply ratAdd_eqRat_compat. apply eqRat_refl. apply ratAdd_eqRat_compat. apply eqRat_refl. eapply IHlsa. eapply eqRat_symm. eapply eqRat_trans. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_l. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_l. apply eqRat_refl. apply eqRat_refl. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_l. apply eqRat_refl. apply eqRat_refl. simpl. eapply eqRat_trans. eapply fold_add_body_eq; intuition. eapply eqRat_refl. eapply fold_add_init_0. simpl. eapply eqRat_trans. eapply fold_add_init_0. eapply eqRat_trans. eapply ratAdd_eqRat_compat. apply eqRat_refl. eapply eqRat_trans. eapply fold_add_body_eq; intuition. apply ratAdd_0_r. apply eqRat_refl. apply eqRat_symm. eapply fold_add_eq. eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply fold_add_init_0. eapply eqRat_refl. eapply eqRat_symm. eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply fold_add_init_0. eapply eqRat_refl. repeat rewrite <- ratAdd_assoc. eapply ratAdd_eqRat_compat. repeat rewrite (ratAdd_assoc (f a b)). eapply ratAdd_eqRat_compat; intuition. eapply ratAdd_comm. eapply eqRat_refl. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool