proposition: Lemma supp_ins k v (s : fmap) : supp (ins k v s) =i predU (pred1 k) (mem (supp s)).
proof: Proof. case: s => s H x; rewrite /supp inE /=. elim: s x k v H=>[|[k1 v1] s IH] //= x k v H. case: ifP=>H1 /=; first by rewrite inE. case: ifP=>H2 /=; first by rewrite !inE (eqP H2) orbA orbb. by rewrite !inE (IH _ _ _ (path_sorted H)) orbCA. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)