Definition path_inv_rotate_lr {X} {a b c:X} (r:a = b) (p:b = c) (q:a = c) : q = r @ p -> q @ !p = r. Proof. intros e. destruct p. destruct q. rewrite pathscomp0rid in e. exact e. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.