proposition: Lemma sin_lb_ge_0 : forall a:R, 0 <= a -> a <= PI / 2 -> 0 <= sin_lb a.
proof: Proof. intros; case (Rtotal_order 0 a); intro. - left; apply sin_lb_gt_0; assumption. - elim H1; intro. + rewrite <- H2; unfold sin_lb; unfold sin_approx; unfold sum_f_R0; unfold sin_term; repeat rewrite pow_ne_zero. * unfold Rdiv; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; right; reflexivity. * discriminate. * discriminate. * discriminate. * discriminate. + elim (Rlt_irrefl 0 (Rle_lt_trans 0 a 0 H H2)). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt