m n : Nat
⊢ ↑m % ↑(succ n) + -↑(succ n) * -↑(m / succ n) = ↑m
m n : Nat
⊢ mod (ofNat m) -[n+1] + -[n+1] * div (ofNat m) -[n+1] = ofNat m
show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
m n : Nat
⊢ ↑m % ↑(succ n) + ↑(succ n) * ↑(m / succ n) = ↑m
m n : Nat
⊢ ↑m % ↑(succ n) + -↑(succ n) * -↑(m / succ n) = ↑m
rw [Int.neg_mul_neg]
no goals
m n : Nat
⊢ ↑m % ↑(succ n) + ↑(succ n) * ↑(m / succ n) = ↑m
exact congrArg ofNat (Nat.mod_add_div ..)
m n : Nat
⊢ -↑(succ m % n) + ↑n * -↑(succ m / n) = -↑(succ m)
m n : Nat
⊢ mod -[m+1] (ofNat n) + ofNat n * div -[m+1] (ofNat n) = -[m+1]
show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
m n : Nat
⊢ -(↑(succ m % n) + ↑n * ↑(succ m / n)) = -↑(succ m)
m n : Nat
⊢ -↑(succ m % n) + ↑n * -↑(succ m / n) = -↑(succ m)
rw [Int.mul_neg, ← Int.neg_add]
m n : Nat
⊢ -↑(succ m % succ n) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)
m n : Nat
⊢ mod -[m+1] -[n+1] + -[n+1] * div -[m+1] -[n+1] = -[m+1]
show -(↑(succ m % succ n) : Int) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)
m n : Nat
⊢ -(↑(succ m % succ n) + ↑(succ n) * ↑(succ m / succ n)) = -↑(succ m)
m n : Nat
⊢ -↑(succ m % succ n) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)
rw [Int.neg_mul, ← Int.neg_add]