proposition: Lemma pvalUnX x y : valid (x \+ psub y) -> pval x \+ y = pval (x \+ psub y).
proof: Proof. by rewrite joinC=>/pvalXUn <-; rewrite joinC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)