m n : Nat
H : n % m = 0
⊢ n = m * (n / m)
m n : Nat
H : n % m = 0
⊢ m ∣ n
exists n / m
m n : Nat
H : n % m = 0
this : n = n % m + m * (n / m)
⊢ n = m * (n / m)
m n : Nat
H : n % m = 0
⊢ n = m * (n / m)
have := (mod_add_div n m).symm
no goals
m n : Nat
H : n % m = 0
this : n = n % m + m * (n / m)
⊢ n = m * (n / m)
rwa [H, Nat.zero_add] at this