proposition: Lemma sepxxA x y z : valid (x \+ (y \+ z)) -> sep y z -> sep x (y \+ z) -> (((sep x (y \+ z) * sep x (z \+ y)) * (sep y (x \+ z) * sep y (z \+ x))) * ((sep z (x \+ y) * sep z (y \+ x)) * (sep (y \+ z) x * sep (z \+ y) x))) * (((sep (x \+ z) y * sep (z \+ x) y) * (sep (x \+ y) z * sep (y \+ x) z)) * (((sep x y * sep y x) * (sep x z * sep z x)))) * (sep y z * sep z y).
proof: Proof. rewrite joinA=> V; rewrite {1}(@sepC x) ?(validLE3 V) // => S1 S2. by apply: (sepAxx V); rewrite (joinC x) joinAC in V; rewrite !(sepAxx V S1 S2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)