[STATEMENT]
lemma arctan_minus: "arctan (- x) = - arctan x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arctan (- x) = - arctan x
[PROOF STEP]
using arctan [of "x"]
[PROOF STATE]
proof (prove)
using this:
- (pi / 2) < arctan x \<and> arctan x < pi / 2 \<and> tan (arctan x) = x

goal (1 subgoal):
 1. arctan (- x) = - arctan x
[PROOF STEP]
by (auto simp: arctan_unique)