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