case a
m k : ℕ+
h : k ∣ m
⊢ ↑(k * divExact m k) = ↑m
m k : ℕ+
h : k ∣ m
⊢ k * divExact m k = m
apply PNat.eq
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * ↑(divExact m k) = ↑m
case a
m k : ℕ+
h : k ∣ m
⊢ ↑(k * divExact m k) = ↑m
rw [mul_coe]
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * succ (div m k) = ↑m
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * ↑(divExact m k) = ↑m
change (k : ℕ) * (div m k).succ = m
no goals
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * succ (div m k) = ↑m
rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]