proposition: Lemma sin_pos_tech : forall x, 0 < x < 2 -> 0 < sin x.
proof: Proof. intros x [int1 int2]. assert (lo : 0 <= x) by (apply Rlt_le; assumption). assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); lra). destruct (pre_sin_bound _ 0 lo up) as [t _]; clear lo up. apply Rlt_le_trans with (2:= t); clear t. unfold sin_approx; simpl sum_f_R0; unfold sin_term; simpl. match goal with |- _ < ?a => replace a with (x * (1 - x^2/6)) by (simpl; field) end. assert (t' : x ^ 2 <= 4). { replace 4 with (2 ^ 2) by field. apply (pow_incr x 2); split; apply Rlt_le; assumption. } apply Rmult_lt_0_compat;[assumption | 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