proposition: Lemma path_supp_ins k1 k v (s : fmap) : ord k1 k -> path ord k1 (supp s) -> path ord k1 (supp (ins k v s)).
proof: Proof. case: s=>s p. elim: s p k1 k v=>[| [k2 v2] s IH] //= p k1 k v H2; first by rewrite H2. case/andP=>H3 H4. have H5: path ord k1 (map key s) by apply: ord_path H4. rewrite /supp /=; case: (totalP k k2)=>H /=. - by rewrite H2 H H4. - by rewrite H2 (eqP H) H4. rewrite H3 /=. have H6: sorted ord (map key s) by apply: path_sorted H5. by move: (IH H6 k2 k v H H4); case: s {IH p H4 H5} H6. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)