proposition: Lemma fmap_zip_with_r (g : C → B) l k : (∀ x y, g (f x y) = y) → length k ≤ length l → g <$> zip_with f l k = k.
proof: Proof. revert l. induction k; intros [|??] ??; f_equal/=; auto with lia. Qed.
imports: stdpp(options)