rw [← inverse_append]
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (append (inverse p) (inverse (inverse q)))
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (inverse (append (inverse q) p))