proposition: Lemma sin_gt_x x : x < 0 -> x < sin x.
proof: Proof. intros. pose proof (sin_lt_x (- x)). pose proof (sin_neg x). lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia