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

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