proposition: Lemma valid_psubUnX x y : valid (x \+ psub y) = valid (pval x \+ y) && D (pval x) y.
proof: Proof. by rewrite -{1}(psub_pval x) valid_psubU. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)