dsimp [prev, rotate, inv]
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ prev (next A (Path.cons' A B✝ A e p)) (rotate A (Path.cons' A B✝ A e p)) = A
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.inverse (Path.snoc p e)) = A