proposition: Lemma path_mapk m k: path ord k (supp m) -> path ord (f k) (supp (mapk m)).
proof: Proof. elim/fmap_ind': m k =>// k1 v1 s P IH k. rewrite {1}/supp //= {1}seqof_ins // /= => /andP [H]; move/IH=>H1. by rewrite /mapk foldf_ins // /supp /= seqof_ins //= H1 andbT (Hf H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)