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

State before:
a : ℤ
n : ℕ
b : ℤ
⊢ mod2 (mod2 a n - b) n = mod2 (a - b) n
Tactic:
sorry
State after:
no goals