proposition: Lemma cos_bound : forall (a : R) (n : nat), - PI / 2 <= a -> a <= PI / 2 -> cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1)).
proof: Proof. intros a n lower upper; apply pre_cos_bound. - apply Rle_trans with (2 := lower). apply Rmult_le_reg_r with 2; [lra |]. replace ((-PI/2) * 2) with (-PI) by field. assert (t := PI_4); lra. - apply Rle_trans with (1 := upper). apply Rmult_le_reg_r with 2; [lra | ]. replace ((PI/2) * 2) with PI by field. generalize PI_4; intros; lra. 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