proposition: Lemma fold_add_nat_Permutation : forall (A : Set)(f : A -> nat)(ls1 ls2 : list A), Permutation ls1 ls2 -> fold_left (fun acc a => acc + (f a))%nat ls1 O = fold_left (fun acc a => acc + (f a))%nat ls2 O.
proof: Proof. induction 1; intuition; simpl in *. rewrite fold_add_init_nat. symmetry. rewrite fold_add_init_nat. symmetry. f_equal. eauto. rewrite Nat.add_comm. trivial. Qed.
imports: FCF.FCF Permutation