proposition: Lemma fold_left_comb (A B C D : Type) (f : B -> C -> D) (g : A -> D -> A) (l1 : list C) (l2 : list B) (i : A) : fold_left (fun x y => fold_left (fun x1 y1 => g x1 (f y y1)) l1 x) l2 i = fold_left g (fold_right (fun y x => (map (f y) l1)++x) nil l2) i .
proof: Proof. revert i; elim l2; simpl; auto; clear l2. intros b l2 Hrec i. rewrite Hrec. rewrite fold_left_app. apply f_equal2 with (f := fold_left g); auto. generalize i; elim l1; simpl; auto; clear l1 Hrec. Qed.
imports: ZArith List