proposition: Lemma pleq_joinl {x1 x2} : [pcm x2 <= x1 \+ x2].
proof: Proof. by rewrite joinC; apply: pleq_joinr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)