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