proposition: Lemma cos_ge_0 : forall x:R, - (PI / 2) <= x -> x <= PI / 2 -> 0 <= cos x.
proof: Proof. intros x H1 H2; elim H1; intro H3; [ elim H2; intro H4; [ left; apply (cos_gt_0 x H3 H4) | rewrite H4; right; symmetry in |- *; apply cos_PI2 ] | rewrite <- H3; rewrite cos_neg; right; symmetry in |- *; apply cos_PI2 ]. 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