proposition: Lemma valid_psubU (x y : V) : valid (psub x \+ psub y) = valid (x \+ y) && D x y.
proof: Proof. case: X=>pval psub [H1 H2 H3 H4]; apply/idP/idP; first by apply: H1. by case/andP; apply: pfV2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)