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