proposition: Lemma sep0x x y : valid (x \+ y) -> sep x y -> sep Unit y.
proof: Proof. rewrite joinC=>V. by rewrite -!(@sepC y) ?unitR ?(validE2 V) //; apply: sepx0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)