proposition: Lemma zip_with_app_r l k1 k2 : zip_with f l (k1 ++ k2) = zip_with f (take (length k1) l) k1 ++ zip_with f (drop (length k1) l) k2.
proof: Proof. revert l. induction k1; intros [|??]; f_equal/=; auto. Qed.
imports: stdpp(options)