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

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

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