m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
⊢ n % k % m = (n % k + k * (n / k)) % m
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
⊢ n % k % m = n % m
conv =>
rhs
rw [← mod_add_div n k]
case intro
m✝ n✝ k n m t : ℕ
⊢ n % (m * t) % m = (n % (m * t) + m * t * (n / (m * t))) % m
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
⊢ n % k % m = (n % k + k * (n / k)) % m
rcases h with ⟨t, rfl⟩
no goals
case intro
m✝ n✝ k n m t : ℕ
⊢ n % (m * t) % m = (n % (m * t) + m * t * (n / (m * t))) % m
rw [mul_assoc, add_mul_mod_self_left]