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