proposition: Lemma acos_atan : forall x, 0 < x -> acos x = atan (sqrt (1 - x²) / x).
proof: Proof. intros x. unfold acos; repeat case Rle_dec; [lra | |]. - intros Hx1 Hx2 Hx3. pose proof Rsqr_bounds_le x 1 ltac:(lra)as Hxsqr. rewrite Rsqr_1 in Hxsqr. rewrite sqrt_neg_0 by lra. replace (0/x) with 0 by (field;lra). rewrite atan_0; reflexivity. - intros Hx1 Hx2 Hx3. pose proof atan_inv (sqrt (1 - x²) / x) as Hatan. pose proof Rsqr_bounds_lt 1 x ltac:(lra)as Hxsqr. rewrite Rsqr_1 in Hxsqr. replace (/ (sqrt (1 - x²) / x)) with (x/sqrt (1 - x²)) in Hatan. + rewrite Hatan; [field|]. apply Rdiv_lt_0_compat; [|assumption]. apply sqrt_lt_R0; lra. + field; split. * lra. * assert(sqrt (1 - x²) >0) by (apply sqrt_lt_R0; lra); lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia