proposition: Lemma dom_mapUn (x y : U) : dom_map (x \+ y) = dom_map x \+ dom_map y.
proof: Proof. case W : (valid (x \+ y)); first by rewrite /dom_map omapUn. rewrite /dom_map; move/invalidE: (negbT W)=>->; rewrite omap_undef. case: validUn W=>//. - by move/invalidE=>->; rewrite omap_undef undef_join. - by move/invalidE=>->; rewrite omap_undef join_undef. move=>k D1 D2 _; suff : ~~ valid (dom_map x \+ dom_map y). - by move/invalidE=>->. by case: validUn=>// _ _ /(_ k); rewrite !dom_mapE=>/(_ D1); rewrite D2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)