add map_zip_diag and the lemmas required for that

Is map_fmap_omap truly new? I was surprised to not find an existing lemma like that.