proposition: Lemma cos_lt_0 : forall x:R, PI / 2 < x -> x < 3 * (PI / 2) -> cos x < 0.
proof: Proof. intros x H1 H2; rewrite <- Ropp_0; rewrite <- (Ropp_involutive (cos x)); apply Ropp_lt_gt_contravar; rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI). - rewrite cos_period; apply cos_gt_0. + replace (- (PI / 2)) with (- PI + PI / 2) by field. unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_lt_compat_l; assumption. + unfold Rminus in |- *; rewrite Rplus_comm; replace (PI / 2) with (- PI + 3 * (PI / 2)) by field. apply Rplus_lt_compat_l; assumption. - 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