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