cases c
case r240.r240
c : Rotation
⊢ r240 + r240 + c = r240 + (r240 + c)
case r240.r240.r0

⊢ r240 + r240 + r0 = r240 + (r240 + r0)

case r240.r240.r120

⊢ r240 + r240 + r120 = r240 + (r240 + r120)

case r240.r240.r240

⊢ r240 + r240 + r240 = r240 + (r240 + r240)