proposition: Lemma fold_add_init_nat : forall (A : Set)(f : A -> nat)(ls : list A)(init : nat), (fold_left (fun acc a => acc + (f a))%nat ls init = init + fold_left (fun acc a => acc + (f a))%nat ls O)%nat.
proof: Proof. intuition. rewrite <- (Nat.add_0_r init) at 1. rewrite fold_add_init_nat_h. trivial. Qed.
imports: FCF.FCF Permutation