proposition: Lemma validRE3 (x y z : U) : valid (x \+ (y \+ z)) -> (((valid x * valid y) * (valid z * valid (x \+ y))) * ((valid (x \+ z) * valid (y \+ x)) * (valid (y \+ z) * valid (z \+ x)))) * (((valid (z \+ y) * valid (x \+ (y \+ z))) * (valid (x \+ y \+ z) * valid (x \+ (z \+ y)))) * ((valid (x \+ z \+ y) * valid (y \+ (x \+ z))) * (valid (y \+ x \+ z) * valid (y \+ (z \+ x))))) * (((valid (y \+ z \+ x) * valid (z \+ (x \+ y))) * (valid (z \+ x \+ y) * valid (z \+ (y \+ x)))) * valid (z \+ y \+ x)).
proof: Proof. by rewrite {1}joinA; apply: validLE3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)