proposition: Lemma pleq_joinxK (V : cpcm) (x x1 x2 : V) : valid (x2 \+ x) -> [pcm x1 \+ x <= x2 \+ x] -> [pcm x1 <= x2].
proof: Proof. by move=>W [a]; rewrite joinAC=>/(joinKx W) ->; exists a. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)