proposition: Lemma tan_lt_0 : forall x:R, - (PI / 2) < x -> x < 0 -> tan x < 0.
proof: Proof. intros x H1 H2; unfold tan in |- *; generalize (cos_gt_0 x H1 (Rlt_trans x 0 (PI / 2) H2 PI2_RGT_0)); intro H3; rewrite <- Ropp_0; replace (sin x / cos x) with (- (- sin x / cos x)). - rewrite <- sin_neg; apply Ropp_gt_lt_contravar; change (0 < sin (- x) / cos x) in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat. + apply sin_gt_0. * rewrite <- Ropp_0; apply Ropp_gt_lt_contravar; assumption. * apply Rlt_trans with (PI / 2). -- rewrite <- (Ropp_involutive (PI / 2)); apply Ropp_gt_lt_contravar; assumption. -- apply PI2_Rlt_PI. + apply Rinv_0_lt_compat; assumption. - unfold Rdiv in |- *; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg