repeat rfl
case r240.r240.s0

⊢ r240 + r240 +ᵥ s0 = r240 +ᵥ (r240 +ᵥ s0)

case r240.r240.s120

⊢ r240 + r240 +ᵥ s120 = r240 +ᵥ (r240 +ᵥ s120)

case r240.r240.s240

⊢ r240 + r240 +ᵥ s240 = r240 +ᵥ (r240 +ᵥ s240)
no goals