proposition: Lemma subPCM_cancel (x1 x2 x : U) : valid (x1 \+ x) -> x1 \+ x = x2 \+ x -> x1 = x2.
proof: Proof. move=>W E; move: (W) (W); rewrite {1}E !(valid_sep U)=>/andP [W2 D2] /andP [W1 D1]. move: E; rewrite -(psub_pval U x1) -(psub_pval U x2) -(psub_pval U x). rewrite -pfjoin // -[R in _ = R]pfjoin //; move/psub_inj. by rewrite valid_psub W1 sepU0 // => /(_ (erefl _)) /(joinKx W1) ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)