{A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : (p = r^ @ q) <~> (r @ p = q) := Build_Equiv _ _ (moveR_Mp p q r) _. Global Instance isequiv_moveR_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : IsEquiv (moveR_pM p q r). Proof. destruct p. apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.