proposition: Lemma zunit_ins f k v : zip_unit (ins k v f) = ins k (unit_f k v) (zip_unit f).
proof: Proof. case: f=>s H; apply/fmapE=>/=; rewrite /zip_unit'. elim: s k v H=>[|[k1 v1] s IH] //= k v H. rewrite eq_sym; case: ordP=>//= O. by rewrite IH // (path_sorted H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)