proposition: Lemma umpleq_asym x y : [pcm x <= y] -> [pcm y <= x] -> x = y.
proof: Proof. case=>a -> [b]; case W : (valid x); last first. - by move/invalidE: (negbT W)=>->; rewrite undef_join. rewrite -{1 2}[x]unitR -joinA in W *. by case/(joinxK W)/esym/join0E=>->; rewrite unitR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)