Theorem: ℤθ.my_intCast_neg_succ_of_nat (Mordell4/CubicRing.lean)

State before:
a b c : ℤθ
⊢ ∀ (n : ℕ), intCast (-↑(n + 1)) = neg (natCast (n + 1))
Tactic:
intro n
State after:
a b c : ℤθ
n : ℕ
⊢ intCast (-↑(n + 1)) = neg (natCast (n + 1))

State before:
a b c : ℤθ
n : ℕ
⊢ intCast (-↑(n + 1)) = neg (natCast (n + 1))
Tactic:
rfl
State after:
no goals