rw [← neg_inj]
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
j : ℕ
g : ℤ
hg0 : 1 ≤ j
hg12 : 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * g + 1) ∨ 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * g + 2)
⊢ -↑(Int.toNat (-n)) = n
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
p6 : 1 ≤ Int.toNat (-n)
j : ℕ
g : ℤ
hg0 : 1 ≤ j
hg12 : 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * g + 1) ∨ 3 * ↑(Int.toNat (-n)) = 3 ^ j * (3 * g + 2)
⊢ - -↑(Int.toNat (-n)) = -n