proposition: Lemma cancelxM t1 t2 x : (x \+ mx t1 = mx t2) <-> (t1 = t2) * (x = Unit).
proof: Proof. by rewrite joinC cancelMx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)