proposition: Lemma zip_with_app_l l1 l2 k : zip_with f (l1 ++ l2) k = zip_with f l1 (take (length l1) k) ++ zip_with f l2 (drop (length l1) k).
proof: Proof. revert k. induction l1; intros [|??]; f_equal/=; auto. by destruct l2. Qed.
imports: stdpp(options)