Theorem: FinInt.add_comm (MLIR/Util/FinInt.lean)

State before:
sz : ℕ
n m : FinInt sz
⊢ n + m = m + n
Tactic:
simp [HAdd.hAdd, add_comm']
State after:
no goals