proposition: Lemma sin_lt_0 : forall x:R, PI < x -> x < 2 * PI -> sin x < 0.
proof: Proof. intros x H1 H2; rewrite <- Ropp_0; rewrite <- (Ropp_involutive (sin x)); apply Ropp_lt_gt_contravar; rewrite <- neg_sin; replace (x + PI) with (x - PI + 2 * INR 1 * PI); [ rewrite (sin_period (x - PI) 1); apply sin_gt_0; [ replace (x - PI) with (x + - PI); [ rewrite Rplus_comm; replace 0 with (- PI + PI); [ apply Rplus_lt_compat_l; assumption | ring ] | ring ] | replace (x - PI) with (x + - PI); rewrite Rplus_comm; [ pattern PI at 2 in |- *; replace PI with (- PI + 2 * PI); [ apply Rplus_lt_compat_l; assumption | ring ] | ring ] ] | unfold INR 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