proposition: Lemma cancPR' (P : U -> Prop) (s1 s2 t1 t2 : U) : precise P -> s1 \+ t1 = s2 \+ t2 -> P t1 -> P t2 -> valid (s1 \+ t1) -> (s1 = s2) * (t1 = t2).
proof: Proof. by move=>H E H1 H2 V; apply: cancPR H V H1 H2 E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)