proposition: Lemma derivable_pt_asin : forall x, -1 < x < 1 -> derivable_pt asin x.
proof: Proof. intros x H. eapply (derivable_pt_recip_interv sin asin (-PI/2) (PI/2)); [shelve ..|]. rewrite <- (pr_nu sin (asin x) (derivable_pt_sin (asin x))). rewrite derive_pt_sin. pose proof asin_bound_lt x ltac:(lra) as HxB3. unfold asin in *. destruct (Rle_dec x (-1)); destruct (Rle_dec 1 x); [lra .. |]. apply Rgt_not_eq; apply cos_gt_0; lra. Unshelve. - pose proof PI_RGT_0 as HPi; lra. - rewrite Rdiv_opp_l,sin_antisym,sin_PI2; lra. - clear x H; intros x Ha Hb. rewrite Rdiv_opp_l; apply asin_bound. - 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. - intros x1 x2 Ha Hb Hc. apply sin_increasing_1; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia