Lemma pathscomp_cancel_right {X : UU} {x y z : X} (p q : x = y) (s : y = z) : p @ s = q @ s -> p = q. Proof. intros e. induction s. refine (_ @ e @ _). - apply pathsinv0, pathscomp0rid. - apply pathscomp0rid. Defined.