proposition: Lemma fold_add_f_inverse : forall (B : Set)(ls : list A)(f : A -> B)(f_inv : B -> A) fa init1 init2, (init1 == init2) -> (forall a, In a ls -> f_inv (f a) = a) -> fold_left (fun r b => r + fa (f_inv b)) (map f ls) init1 == fold_left (fun r a => r + (fa a)) ls init2.
proof: Proof. induction ls; intuition; simpl in *. eapply IHls; eauto. rewrite H0. eapply ratAdd_eqRat_compat; eauto. eapply eqRat_refl. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool