proposition: Lemma pfV3 (U : pcm) V (D : rel U) (f : @morphism U V D) x y z: valid (x \+ y \+ z) -> D x y -> D (x \+ y) z -> valid (f x \+ f y \+ f z).
proof: Proof. by move=>W D1 D2;rewrite -pfjoin ?(validL W) // pfV2 //=. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)