proposition: Lemma sepAxx x y z : valid (x \+ y \+ z) -> sep x y -> 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. move=>V S1 S2; rewrite S1 S2 !(sepAx23_helper V S1 S2). rewrite -(sepC (validL V)) S1. rewrite (joinC y) -sepC // S2; rewrite -(joinC y) sepC 1?joinC ?joinA // (sepAx23_helper V S1 S2). by rewrite -(joinC x) sepC 1?joinAC // (sepAx23_helper V S1 S2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)