Definition pathsinv0_to_right {X} {x y z:X} (p:y = x) (q:y = z) (r:x = z) : q = p @ r -> !p @ q = r. Proof. intros e. induction p, q. exact e. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.