[STATEMENT]
lemma d_delta_arctan_upper_31_pos: "x \<noteq> 0 \<Longrightarrow> diff_delta_arctan_upper_31 x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 < diff_delta_arctan_upper_31 x
[PROOF STEP]
unfolding diff_delta_arctan_upper_31_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 < 64 / (x\<^sup>2 * (15 + 70 * x\<^sup>2 + 63 * x ^ 4)\<^sup>2 * (1 + x\<^sup>2))
[PROOF STEP]
by (auto simp: divide_simps zero_less_mult_iff add_pos_pos add_nonneg_eq_0_iff)