proposition: Lemma validE2 (x y : U) : valid (x \+ y) -> (valid x * valid y) * (valid (x \+ y) * valid (y \+ x)).
proof: Proof. by move=>X; rewrite (validL X) (validR X) X joinC X. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)