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