no goals
x✝ : Int
n✝ : Nat
⊢ x✝ / sign ↑(succ n✝) = x✝ * sign ↑(succ n✝)
simp [sign, Int.mul_one]
no goals
x✝ : Int
⊢ x✝ / sign 0 = x✝ * sign 0
simp [sign, Int.mul_zero]
no goals
x✝ : Int
a✝ : Nat
⊢ x✝ / sign -[a✝+1] = x✝ * sign -[a✝+1]
simp [sign, Int.mul_neg, Int.mul_one]