proposition: Lemma umfoldlUn a z0 d f1 f2 : valid (f1 \+ f2) -> {in dom f1 & dom f2, forall x y, ord x y} -> um_foldl a z0 d (f1 \+ f2) = um_foldl a (um_foldl a z0 d f1) d f2.
proof: Proof. move: f2; apply: um_indb=>[W H|W H|k v f2 IH W' P W H]. - by rewrite join_undef !umfoldl_undef. - by rewrite unitR umfoldl0. rewrite -(joinC f2) joinA in W *; rewrite umfoldlUnPt //; last first. - apply/allP=>x; rewrite domUn inE (validL W). case/orP=>[/H|]; last by apply: P. by apply; rewrite domPtUn inE joinC W' eq_refl. rewrite umfoldlUnPt ?(validAR W) //; last by apply/allP. rewrite (IH (validL W)) // => k1 k2 D1 D2; apply: H D1 _. by rewrite domPtUn inE joinC W' D2 orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)