proposition: Theorem fold_add_flatten : forall (A : Set)(ls : list (list A)) f init, fold_left (fun a b => a + f b) (flatten ls) init == fold_left (fun a b => a + (sumList b f)) ls init.
proof: Proof. induction ls; intuition idtac; simpl in *. reflexivity. rewrite fold_left_app. rewrite IHls. apply fold_left_init_eq. intuition idtac. apply ratAdd_eqRat_compat; intuition idtac. reflexivity. unfold sumList. rewrite <- fold_add_init. apply fold_left_init_eq. intuition idtac. apply ratAdd_eqRat_compat; intuition idtac. reflexivity. rewrite <- ratAdd_0_r. reflexivity. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation