Every panmagic square is magic

A panmagic (pandiagonal) square is in particular a magic square.

By definition IsPanMagic M s requires every row and every column to sum to $s$ (the semi-magic condition) and, in addition, every broken diagonal in both directions to sum to $s$. The two main diagonals are the broken diagonals of offset $0$, so both main diagonal sums equal $s$, which is exactly the extra content of IsMagic M s over IsSemiMagic M s.

Formalization Note brokenDiagSum M k is $\sum_i M_{i,\, i+k}$ with the column index read modulo $n$, so brokenDiagSum M 0 = diagSum M. For the anti-diagonal one uses brokenAntiDiagSum M 0, i.e. $\sum_i M_{i,\, n-1-i}$, which is antiDiagSum M. Only $n \neq 0$ is needed so that Fin n carries the additive structure used to speak of offsets.