proposition: Lemma asin_inv_sqrt2 : asin (/sqrt 2) = PI/4.
proof: Proof. rewrite asin_atan. { pose proof sqrt2_neq_0 as SH. rewrite Rsqr_pow2, pow_inv, <- Rsqr_pow2, Rsqr_sqrt; try lra. replace (1 - /2) with (/2) by lra. rewrite sqrt_inv. now rewrite <- atan_1; apply f_equal; field. } split. { apply (Rlt_trans _ 0); try lra. apply Rinv_0_lt_compat; apply sqrt_lt_R0; lra. } replace 1 with (/ sqrt 1). { 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