m : Nat
b : Int
bpos : 0 < b
⊢ -[m+1] % b = b - (↑m % b + 1)
m : Nat
b : Int
bpos : 0 < b
⊢ -[m+1] % b = b - 1 - ↑m % b
rw [Int.sub_sub, Int.add_comm]
no goals
m : Nat
b : Int
bpos : 0 < b
⊢ -[m+1] % b = b - (↑m % b + 1)
match b, eq_succ_of_zero_lt bpos with
| _, ⟨n, rfl⟩ => rfl
no goals
m : Nat
b : Int
n : Nat
bpos : 0 < ↑(succ n)
⊢ -[m+1] % ↑(succ n) = ↑(succ n) - (↑m % ↑(succ n) + 1)
rfl