fact: Definition equiv_moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : (r^ @ q = p) <~> (q = r @ p) := Build_Equiv _ _ (moveL_Mp p q r) _.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics