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

State before:
sz : ℕ
n m : FinInt sz
⊢ add n m = add m n
Tactic:
simp [add, addfull_comm]
State after:
no goals