n m k : Int
h : m ∣ k
⊢ n % k % m = (n % k + k * (n / k)) % m
n m k : Int
h : m ∣ k
⊢ n % k % m = n % m
conv => rhs; rw [← emod_add_ediv n k]
no goals
n m k : Int
h : m ∣ k
⊢ n % k % m = (n % k + k * (n / k)) % m
match k, h with
| _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]
no goals
n m k : Int
h : m ∣ k
t : Int
⊢ n % (m * t) % m = (n % (m * t) + m * t * (n / (m * t))) % m
rw [Int.mul_assoc, add_mul_emod_self_left]