proposition: Lemma valid_xpsubU x y : valid (xpsub x \+ xpsub y) -> orth2 x y.
proof: Proof. rewrite /xpsub {1}/valid /= -?lock /xsep_valid /= !pcm_joinE /= /xsep_join !unlock /xsep_join' /= -pcmE. by case: decP=>Hx; case: decP=>Hy; case H: (orth2 x y) Hx Hy; rewrite /= ?tpcmE //=; case/andP: H=>V H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)