proposition: Lemma sin_gt_cos_7_8 : sin (7 / 8) > cos (7 / 8).
proof: Proof. assert (lo1 : 0 <= 7/8) by lra. assert (up1 : 7/8 <= 4) by lra. assert (lo : -2 <= 7/8) by lra. assert (up : 7/8 <= 2) by lra. destruct (pre_sin_bound _ 0 lo1 up1) as [lower _ ]. destruct (pre_cos_bound _ 0 lo up) as [_ upper]. apply Rle_lt_trans with (1 := upper). apply Rlt_le_trans with (2 := lower). unfold cos_approx, sin_approx. simpl sum_f_R0. unfold cos_term, sin_term; simpl fact; rewrite !INR_IZR_INZ. simpl plus; simpl mult; simpl Z_of_nat. field_simplify. match goal with |- IZR ?a / ?b < ?c / ?d => apply Rmult_lt_reg_r with d;[apply (IZR_lt 0); reflexivity | unfold Rdiv at 2; rewrite Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_comm; [ |apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity ]]; apply Rmult_lt_reg_r with b;[apply (IZR_lt 0); reflexivity | ] end. unfold Rdiv; rewrite !Rmult_assoc, Rinv_l, Rmult_1_r; [ | apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity]. rewrite <- !mult_IZR. apply IZR_lt; reflexivity. 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