proposition: Lemma seqof_ins_perm k v (s : fmap) : k \notin supp s -> perm (seq_of (ins k v s)) ((k, v) :: seq_of s).
proof: Proof. case: s; elim=>[|[k1 v1] s IH] //= H; case: ifP=>E //. case: eqP=>[->|N]; first by rewrite /supp /= inE eq_refl. rewrite /supp /= inE negb_or; case/andP=>K1 {}/IH IH. suff S : perm (ins' k v s) [:: (k, v) & s]. - move/(pperm_cons (k1, v1))/pperm_trans: S. by apply; apply: permutation_swap. by apply: IH; apply: path_sorted H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)