proposition: Lemma sin_ge_0 : forall x:R, 0 <= x -> x <= PI -> 0 <= sin x.
proof: Proof. intros x H1 H2; elim H1; intro H3; [ elim H2; intro H4; [ left; apply (sin_gt_0 x H3 H4) | rewrite H4; right; symmetry in |- *; apply sin_PI ] | rewrite <- H3; right; symmetry in |- *; apply sin_0 ]. 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