Theorem: mod_sub_mod (Fl/Lemmas.lean)

State before:
m n k : ℕ
h : k ≤ m
⊢ (m - k) % n = (m - k % n) % n
Tactic:
conv => lhs ; rewrite [← Nat.mod_add_div k n, ← tsub_tsub]
State after:
m n k : ℕ
h : k ≤ m
⊢ (m - k % n - n * (k / n)) % n = (m - k % n) % n

State before:
m n k : ℕ
h : k ≤ m
⊢ (m - k % n - n * (k / n)) % n = (m - k % n) % n
Tactic:
apply sub_mul_mod_self_left
State after:
case h
m n k : ℕ
h : k ≤ m
⊢ n * (k / n) ≤ m - k % n

State before:
case h
m n k : ℕ
h : k ≤ m
⊢ n * (k / n) ≤ m - k % n
Tactic:
apply le_tsub_of_add_le_left
State after:
case h.h
m n k : ℕ
h : k ≤ m
⊢ k % n + n * (k / n) ≤ m

State before:
case h.h
m n k : ℕ
h : k ≤ m
⊢ k % n + n * (k / n) ≤ m
Tactic:
rewrite [Nat.mod_add_div]
State after:
case h.h
m n k : ℕ
h : k ≤ m
⊢ k ≤ m

State before:
case h.h
m n k : ℕ
h : k ≤ m
⊢ k ≤ m
Tactic:
exact h
State after:
no goals