proposition: Lemma domUnPtK k v f : valid (f \+ pts k v) -> all (ord^~k) (dom f) -> dom (f \+ pts k v) = rcons (dom f) k.
proof: Proof. move=>W H; apply: ord_sorted_eq=>//=. - rewrite -(rev_sorted (fun x=>ord^~x)) rev_rcons /=. by rewrite path_min_sorted ?rev_sorted // all_rev. by move=>x; rewrite domUnPt inE W mem_rcons inE eq_sym. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)