proposition: Lemma derivable_pt_acos : forall x, -1 < x < 1 -> derivable_pt acos x.
proof: Proof. intros x H. eapply (derivable_pt_recip_interv_decr cos acos 0 PI); [shelve ..|]. rewrite <- (pr_nu cos (acos x) (derivable_pt_cos (acos x))). rewrite derive_pt_cos. pose proof acos_bound_lt x ltac:(lra) as Hbnd. unfold acos in *. destruct (Rle_dec x (-1)); destruct (Rle_dec 1 x); [lra..|]. apply Rlt_not_eq, Ropp_lt_gt_0_contravar, Rlt_gt. apply sin_gt_0; lra. Unshelve. - pose proof PI_RGT_0 as HPi; lra. - rewrite cos_0; rewrite cos_PI; lra. - clear x H; intros x H1 H2. apply acos_bound. - intros a Ha; reg. - intros x0 H1 H2. unfold comp,id. apply cos_acos. rewrite cos_PI in H1; rewrite cos_0 in H2; lra. - intros x1 x2 H1 H2 H3. pose proof cos_decreasing_1 x1 x2; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia