Solution (source code)

= Solution

This assertion is \b[always true]. Synthetically, either bracketing places three disjoint blocks of order types $\alpha,\beta,\gamma$ in that order. The identity on these blocks is an <order isomorphism>, so both sums have the same <order type>. This proves <associativity of ordinal addition> for successor and limit <ordinals> alike.