proposition: Lemma umfoldrUn a z0 d f1 f2 : valid (f1 \+ f2) -> {in dom f1 & dom f2, forall x y, ord x y} -> um_foldr a z0 d (f1 \+ f2) = um_foldr a (um_foldr a z0 d f2) d f1.
proof: Proof. move: f1; apply: um_indf=>[W H|W H|k v f1 IH W' P W H]. - by rewrite undef_join !umfoldr_undef. - by rewrite unitL umfoldr0. rewrite -!joinA in W *; rewrite umfoldrPtUn //. - rewrite umfoldrPtUn ?(order_path_min (@trans K) P) // (IH (validR W)) //. by move=>k1 k2 D1; apply: H; rewrite domPtUn inE W' D1 orbT. apply/allP=>x; rewrite domUn inE (validR W) /=. case/orP; last by apply: H; rewrite domPtUn inE W' eq_refl. by apply/allP/(order_path_min (@trans K) P). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)