proposition: Lemma rem_ins k1 k2 v (s : fmap) : rem k1 (ins k2 v s) = if k1 == k2 then rem k1 s else ins k2 v (rem k1 s).
proof: Proof. rewrite /rem; case: s => s H /=; case H1: (k1 == k2); rewrite /= fmapE /=. - rewrite (eqP H1) {H1}. elim: s k2 H=>[|[k3 v3] s IH] k2 /= H; rewrite ?eq_refl 1?eq_sym //. case: (ordP k3 k2)=>H1 /=; rewrite ?eq_refl //=; case: (ordP k3 k2) H1=>//= H1 _. by rewrite IH //; apply: path_sorted H. elim: s k1 k2 H1 H=>[|[k3 v3] s IH] k1 k2 H1 /= H; first by rewrite eq_sym H1. case: (ordP k2 k3)=>H2 /=. - rewrite eq_sym H1 /=. case: (ordP k3 k1)=>H3 /=; case: (ordP k2 k3) (H2)=>//=. rewrite -(eqP H3) in H1 *. rewrite -IH //; last by apply: path_sorted H. rewrite last_ins' /= 1?eq_sym ?H1 //. by apply: ord_path H. - by move: H1; rewrite (eqP H2) /= eq_sym => -> /=; rewrite irr eq_refl. case: (ordP k3 k1)=>H3 /=. - case: (ordP k2 k3) H2=>//= H2 _. by rewrite IH //; apply: path_sorted H. - rewrite -(eqP H3) in H1 *. by rewrite IH //; apply: path_sorted H. case: (ordP k2 k3) H2=>//= H2 _. by rewrite IH //; apply: path_sorted H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)