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