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

State before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) ≡ toUint n + toUint m [2^sz]
Tactic:
simp [cong2, toUint_mod2]
State after:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) = mod2 (toUint n + toUint m) sz

State before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) = mod2 (toUint n + toUint m) sz
Tactic:
apply add_toUint
State after:
no goals