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