proposition: Lemma ins_rem k1 k2 v (s : fmap) : ins k1 v (rem k2 s) = if k1 == k2 then ins k1 v s else rem k2 (ins k1 v s).
proof: Proof. move: k1 k2 v s. have L3: forall (x : K) s, path ord x (map key s) -> filter (predCk V x) s = s. - move=>x t; move/notin_path; elim: t=>[|[k3 v3] t IH] //=. rewrite inE negb_or; case/andP=>T1 T2. by rewrite eq_sym T1 IH. have L5: forall (x : K) (v : V) s, sorted ord (map key s) -> ins' x v (filter (predCk V x) s) = ins' x v s. - move=>x v s; elim: s x v=>[|[k' v'] s IH] x v //= H. case H1: (ord x k'). - case H2: (k' == x)=>/=; first by rewrite (eqP H2) irr in H1. by rewrite H1 L3 //; apply: ord_path H1 H. case H2: (k' == x)=>/=. - rewrite (eqP H2) eq_refl in H *. by rewrite L3 //; apply: last_ins' H. rewrite eq_sym H2 H1 IH //. by apply: path_sorted H. move=>k1 k2 v [s H]. case: ifP=>H1; rewrite /ins /rem fmapE /=. - rewrite {k1 H1}(eqP H1). elim: s k2 v H=>[|[k' v'] s IH] //= k2 v H. case H1: (k' == k2)=>/=. - rewrite eq_sym H1 (eqP H1) irr in H *. by rewrite L3 // last_ins'. rewrite eq_sym H1; case: ifP=>H3. - by rewrite L3 //; apply: ord_path H3 H. by rewrite L5 //; apply: path_sorted H. elim: s k1 k2 H1 H=>[|[k' v'] s IH] //= k1 k2 H1 H; first by rewrite H1. case H2: (k' == k2)=>/=. - rewrite (eqP H2) in H *; rewrite H1. case H3: (ord k1 k2)=>/=. - by rewrite H1 eq_refl /= last_ins' // L3 //; apply: ord_path H. by rewrite eq_refl /= IH //; apply: path_sorted H. case H3: (ord k1 k')=>/=; first by rewrite H1 H2. case H4: (k1 == k')=>/=; first by rewrite H1. by rewrite H2 IH //; apply: path_sorted H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)