proposition: Lemma umcompUnf g1 g2 f : valid (g1 \+ g2) -> um_comp (g1 \+ g2) f = um_comp g1 f \+ um_comp g2 f.
proof: Proof. rewrite /um_comp=>Wg; elim/um_indf: f=>[||k v f IH P W]. - by rewrite !umfoldl_undef undef_join. - by rewrite !umfoldl0 unitL. rewrite !umfoldlUn_frame //; try by move=>*; case: (find _ _)=>// a; rewrite joinA. rewrite !unitR !umfoldlPt; case: ifP=>C; last by rewrite !undef_join. rewrite {}IH joinAC [in X in _ = X]joinA [in X in _ = X]joinAC; rewrite -[in X in _ = X]joinA; congr (_ \+ _). case: validUn (Wg)=>// W1 W2 X _; rewrite findUnL //. by case: ifP=>[/X|]; case: dom_find=>// ->; rewrite ?unitL ?unitR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)