repeat {
 cases c
 repeat { rfl }
}
case r240.r0
c : Rotation
⊢ r240 + r0 + c = r240 + (r0 + c)

case r240.r120
c : Rotation
⊢ r240 + r120 + c = r240 + (r120 + c)

case r240.r240
c : Rotation
⊢ r240 + r240 + c = r240 + (r240 + c)
no goals