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