proposition: Lemma umpleq_join a b f : valid (a \+ b) -> [pcm a <= f] -> [pcm b <= f] -> [pcm a \+ b <= f].
proof: Proof. case Vf: (valid f); last by move/invalidE: (negbT Vf)=>->; move: umpleq_undef. move=>W /(umpleqk_pleqE _ Vf) <- /(umpleqk_pleqE _ Vf) <-. rewrite -umfilt_dpredU //. by case=>/= a0 _; move: a0; apply: valid_subdom W. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)