proposition: Lemma psubXUn x y : valid (x \+ psub y) -> x \+ psub y = psub (pval x \+ y).
proof: Proof. by rewrite valid_psubUnX=>/andP [W H]; rewrite pfjoin // psub_pval. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)