proposition: Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x.
proof: Proof. intros; rewrite cos_sin; generalize (Rplus_lt_compat_l (PI / 2) (- (PI / 2)) x H). rewrite Rplus_opp_r; intro H1; generalize (Rplus_lt_compat_l (PI / 2) x (PI / 2) H0); rewrite Rplus_half_diag; intro H2; apply (sin_gt_0 (PI / 2 + x) H1 H2). 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