proposition: Lemma supp_nilE (s : fmap) : (supp s = [::]) <-> (s = nil).
proof: Proof. by split=>[|-> //]; case: s; case=>// H; rewrite fmapE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)