[STATEMENT]
lemma tan_mono_le: "-(pi/2) < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < pi/2 \<Longrightarrow> tan x \<le> tan y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- (pi / 2) < x; x \<le> y; y < pi / 2\<rbrakk> \<Longrightarrow> tan x \<le> tan y
[PROOF STEP]
using less_eq_real_def tan_monotone
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
\<lbrakk>- (pi / 2) < ?y; ?y < ?x; ?x < pi / 2\<rbrakk> \<Longrightarrow> tan ?y < tan ?x

goal (1 subgoal):
 1. \<lbrakk>- (pi / 2) < x; x \<le> y; y < pi / 2\<rbrakk> \<Longrightarrow> tan x \<le> tan y
[PROOF STEP]
by auto