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