Theorem: Nat.mul_sub_mod_right (Algdata/Init/Nat.lean)

State before:
l m n : Nat
⊢ l > 0 → m ≥ n → (l * m - n) % m = (m - n) % m
Tactic:
intro hl hmn
State after:
l m n : Nat
hl : l > 0
hmn : m ≥ n
⊢ (l * m - n) % m = (m - n) % m

State before:
l m n : Nat
hl : l > 0
hmn : m ≥ n
⊢ (l * m - n) % m = (m - n) % m
Tactic:
rw [Nat.mul_comm, mul_sub_mod_left hl hmn]
State after:
no goals