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

case r120
b c : Rotation
⊢ r120 + b + c = r120 + (b + c)

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