proposition: Lemma derive_pt_asin : forall (x : R) (Hxrange : -1 < x < 1), derive_pt asin x (derivable_pt_asin x Hxrange) = 1 / sqrt (1 - x²).
proof: Proof. intros x Hxrange. epose proof (derive_pt_recip_interv sin asin (-PI/2) (PI/2) x _ _ _ _ _ _ _) as Hd. rewrite <- (pr_nu sin (asin x) (derivable_pt_sin (asin x))) in Hd. rewrite <- (pr_nu asin x (derivable_pt_asin x Hxrange)) in Hd. rewrite derive_pt_sin in Hd. rewrite cos_asin in Hd by lra. assumption. Unshelve. - pose proof PI_RGT_0. lra. - rewrite Rdiv_opp_l,sin_antisym,sin_PI2; lra. - intros x1 x2 Ha Hb Hc. apply sin_increasing_1; lra. - intros x0 Ha Hb. pose proof asin_bound x0; lra. - intros a Ha; reg. - intros x0 Ha Hb. unfold comp,id. apply sin_asin. rewrite Rdiv_opp_l,sin_antisym,sin_PI2 in Ha; rewrite sin_PI2 in Hb; lra. - rewrite <- (pr_nu sin (asin x) (derivable_pt_sin (asin x))). rewrite derive_pt_sin. rewrite cos_asin by lra. apply Rgt_not_eq. apply sqrt_lt_R0. pose proof Rsqr_bounds_lt 1 x ltac:(lra) as Hxsqrrange. rewrite Rsqr_1 in Hxsqrrange; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia