proposition: Lemma zip_with_take_both' n1 n2 l k : length l `min` length k ≤ n1 → length l `min` length k ≤ n2 → zip_with f (take n1 l) (take n2 k) = zip_with f l k.
proof: Proof. intros. rewrite zip_with_take_l'; [apply zip_with_take_r' | rewrite take_length]; lia. Qed.
imports: stdpp(options)