proposition: Lemma acos_0 : acos 0 = PI/2.
proof: Proof. unfold acos; repeat case Rle_dec; [lra..|]. intros Hx1 Hx2. replace (0/_) with 0. { rewrite atan_0; field. } field. rewrite Rsqr_pow2; field_simplify (1 - 0^2). rewrite sqrt_1; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia