proposition: Lemma tan_increasing : forall x y, -PI/2 < x -> x < y -> y < PI/2 -> tan x < tan y.
proof: Proof. intros x y Z_le_x x_lt_y y_le_1. assert (x_encad : -PI/2 < x < PI/2). { split ; [assumption | apply Rlt_trans with (r2:=y) ; assumption]. } assert (y_encad : -PI/2 < y < PI/2). { split ; [apply Rlt_trans with (r2:=x) ; intuition | intuition ]. } assert (local_derivable_pt_tan : forall x, -PI/2 < x < PI/2 -> derivable_pt tan x). { intros ; apply derivable_pt_tan ; intuition. } apply derive_increasing_interv with (a:=-PI/2) (b:=PI/2) (pr:=local_derivable_pt_tan) ; intuition. { lra. } assert (Temp := pr_nu tan t (derivable_pt_tan t t_encad) (local_derivable_pt_tan t t_encad)) ; rewrite <- Temp ; clear Temp. assert (Temp := derive_pt_tan t t_encad) ; rewrite Temp ; clear Temp. apply plus_Rsqr_gt_0. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia