proposition: Lemma pprojPV2 x y : valid (x \+ y) = valid (pfst x \+ pfst y) && valid (psnd x \+ psnd y).
proof: Proof. by rewrite (valid_sep X) pcmPV andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)