proposition: Lemma acos_inv_sqrt2 : acos (/sqrt 2) = PI/4.
proof: Proof. rewrite acos_asin. { rewrite asin_inv_sqrt2. lra. } split. { apply Rlt_le. apply (Rlt_trans (-1) 0 (/ sqrt 2)); try lra. apply Rinv_0_lt_compat. apply Rlt_sqrt2_0. } replace 1 with (/ sqrt 1). { apply Rlt_le. apply Rinv_0_lt_contravar. { rewrite sqrt_1; lra. } apply sqrt_lt_1; lra. } rewrite sqrt_1; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia