proposition: Lemma sepAx x y z : valid (x \+ y \+ z) -> sep x y -> sep (x \+ y) z -> sep x (y \+ z) * sep y z.
proof: Proof. by case: sep=>r [[??? H]] V R1 R2 /=; rewrite !(andX (H _ _ _ V R1 R2)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)