proposition: Lemma umpfxE h1 h : valid h1 -> um_prefix h1 h -> exists2 h2, h = h1 \+ h2 & forall x y, x \in dom h1 -> y \in dom h2 -> ord x y.
proof: Proof. move=>V1; case W : (valid h); last first. - move/invalidE: (negbT W)=>-> _. exists undef; first by rewrite join_undef. by rewrite dom_undef. move: h1 h V1 W; apply: um_indf=>[h|h _ W| k v h1 IH W1 /(order_path_min (@trans _)) P h _ W]. - by rewrite valid_undef. - by exists h; [rewrite unitL | rewrite dom0]. case/prefixE=>h2'; rewrite assocsPtUn //= => Eh. set h' := free h k; have W' : valid h' by rewrite validF. have : um_prefix h1 h'. - rewrite /um_prefix assocsF Eh /= eq_refl filter_cat /=. have : forall kv, kv \In assocs h1 -> kv.1 != k. - move=>kv /In_assocs/In_dom H; move/allP/(_ _ H): P. by case: eqP=>// ->; rewrite irr. by move/eq_In_filter=>->; rewrite filter_predT; apply: prefix_cat. case/(IH _ (validR W1) W')=>h2 Eh' H; exists h2. - rewrite -joinA -Eh'; apply/um_eta2/In_find/In_assocs. by rewrite Eh In_cons; left. move=>x y; rewrite domPtUn inE W1 /=; case/orP; last by apply: H. move/eqP=><-{x} Dy. have : y \in dom h' by rewrite Eh' domUn inE -Eh' W' /= Dy orbT. rewrite domF inE; case: (k =P y)=>// /eqP N. rewrite assocs_dom Eh /= inE eq_sym (negbTE N) /=. case/mem_seqP/MapP; case=>a b X -> /=. have {}P : path ord k (map fst (assocs h1 ++ h2')). - by move: (sorted_dom h); rewrite assocs_dom Eh /=. suff {X} : forall x, x \In assocs h1 ++ h2' -> ord k x.1 by move/(_ _ X). apply/allPIn/(order_path_min (x:=(k,v)) (leT:=fun k x=>ord k.1 x.1)). - by move=>???; apply: trans. by rewrite -path_map. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)