proposition: Lemma derive_pt_acos : forall (x : R) (Hxrange : -1 < x < 1), derive_pt acos x (derivable_pt_acos x Hxrange) = -1 / sqrt (1 - x²).
proof: Proof. intros x Hxrange. epose proof (derive_pt_recip_interv_decr cos acos 0 PI x _ _ _ _ _ _ _ ) as Hd. rewrite <- (pr_nu cos (acos x) (derivable_pt_cos (acos x))) in Hd. rewrite <- (pr_nu acos x (derivable_pt_acos x Hxrange)) in Hd. rewrite derive_pt_cos in Hd. rewrite sin_acos in Hd by lra. rewrite Hd; field. apply Rgt_not_eq, Rlt_gt; rewrite <- sqrt_0. pose proof Rsqr_bounds_lt 1 x ltac:(lra) as Hxb; rewrite Rsqr_1 in Hxb. apply sqrt_lt_1; lra. Unshelve. - pose proof PI_RGT_0; lra. - rewrite cos_PI,cos_0; lra. - intros x1 x2 Ha Hb Hc. apply cos_decreasing_1; lra. - intros x0 Ha Hb. pose proof acos_bound x0; lra. - intros a Ha; reg. - intros x0 Ha Hb. unfold comp,id. apply cos_acos. rewrite cos_PI in Ha; rewrite cos_0 in Hb; lra. - rewrite <- (pr_nu cos (acos x) (derivable_pt_cos (acos x))). rewrite derive_pt_cos. rewrite sin_acos by lra. apply Rlt_not_eq; rewrite <- Ropp_0; apply Ropp_lt_contravar; rewrite <- sqrt_0. pose proof Rsqr_bounds_lt 1 x ltac:(lra) as Hxb; rewrite Rsqr_1 in Hxb. apply sqrt_lt_1; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia