proposition: Lemma join0E (x y : mutex) : x \+ y = Unit -> x = Unit /\ y = Unit.
proof: Proof. by case: x y=>[||x][||y]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)