proposition: Lemma sin_lt_x x : 0 < x -> sin x < x.
proof: Proof. intros. pose proof PI2_1. destruct (SIN_bound x), (Rle_or_lt x (PI / 2)); try lra. pose (f x := x - sin x). cut (f 0 < f x); [now unfold f; rewrite sin_0; lra|]. eapply (MVT.derive_increasing_interv 0 (PI/2) (id - sin)%F); try lra. intros t Ht. rewrite derive_pt_minus, derive_pt_id, derive_pt_sin. pose proof (COS_bound t). pose proof cos_0. pose proof (cos_inj 0 t). lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia