proposition: Lemma cancPL (P : U -> Prop) s1 s2 t1 t2 : precise P -> valid (s1 \+ t1) -> P s1 -> P s2 -> s1 \+ t1 = s2 \+ t2 -> (s1 = s2) * (t1 = t2).
proof: Proof. move=>H V H1 H2 E; move: (H _ _ _ _ V H1 H2 E)=>X. by rewrite -X in E *; rewrite (joinxK V E). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)