no goals
a✝ : Nat
⊢ 0 + 0 = 0
simp
m n : Nat
⊢ subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + ↑n + 1) = ↑m + 1
m n : Nat
⊢ fmod ↑(succ m) -[n+1] + -[n+1] * fdiv ↑(succ m) -[n+1] = ↑(succ m)
show subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + n + 1) = (m + 1)
m n : Nat
⊢ ↑(m % succ n) + ↑(succ n * (m / succ n)) + 1 = ↑m + 1
m n : Nat
⊢ subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + ↑n + 1) = ↑m + 1
rw [Int.add_comm _ n, ← Int.add_assoc, ← Int.add_assoc,
  Int.subNatNat_eq_coe, Int.sub_add_cancel]
a✝ : Nat
⊢ -[a✝+1] + 0 * fdiv -[a✝+1] 0 = -[a✝+1]
a✝ : Nat
⊢ fmod -[a✝+1] 0 + 0 * fdiv -[a✝+1] 0 = -[a✝+1]
rw [fmod_zero]
no goals
a✝ : Nat
⊢ -[a✝+1] + 0 * fdiv -[a✝+1] 0 = -[a✝+1]
rfl
m n : Nat
⊢ subNatNat (succ n) (succ (m % succ n)) - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)
m n : Nat
⊢ fmod -[m+1] ↑(succ n) + ↑(succ n) * fdiv -[m+1] ↑(succ n) = -[m+1]
show subNatNat .. - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)
m n : Nat
⊢ -(↑(succ (m % succ n)) + ↑(succ n * (m / succ n))) = -↑(succ m)
m n : Nat
⊢ subNatNat (succ n) (succ (m % succ n)) - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)
rw [Int.subNatNat_eq_coe, ← Int.sub_sub, ← Int.neg_sub, Int.sub_sub, Int.sub_sub_self]
m n : Nat
⊢ -↑(succ m % succ n) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
m n : Nat
⊢ fmod -[m+1] -[n+1] + -[n+1] * fdiv -[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_add]