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