proposition: Lemma valid_psubUn (x y : V) : valid (x \+ y) -> D x y -> valid (psub x \+ psub y).
proof: Proof. by move=>W H; rewrite valid_psubU W H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)