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