proposition: Lemma acos_bound_lt : forall x, -1 < x < 1 -> 0 < acos x < PI.
proof: Proof. intros x xB. pose proof PI_RGT_0. unfold acos; repeat case Rle_dec; try lra. intros Hx1 Hx2. pose proof atan_bound (x / sqrt (1 - x²)); lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia