proposition: Lemma pvalXUn x y : valid (psub x \+ y) -> x \+ pval y = pval (psub x \+ y).
proof: Proof. move=>W; rewrite pfjoin //. move/validL: W; rewrite valid_psub=>/andP [V1 V2]. by rewrite pval_psub. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)