Theorem: rot_state_vsub_vadd' (Instructor/Lectures/grad/case_study_symmetries.lean)

State before:
⊢ ∀ (p1 p2 : State), p1 -ᵥ p2 +ᵥ p2 = p1
Tactic:
_
State after:
no goals