proposition: Lemma Datan_eq_DatanSeq_interv : forall x, -1 < x < 1 -> forall (Pratan:derivable_pt ps_atan x) (Prmymeta:derivable_pt atan x), derive_pt ps_atan x Pratan = derive_pt atan x Prmymeta.
proof: Proof. assert (freq : 0 < tan 1) by apply (Rlt_trans _ _ _ Rlt_0_1 tan_1_gt_1). intros x x_encad Pratan Prmymeta. rewrite pr_nu_var2_interv with (g:=ps_atan) (lb:=-1) (ub:=tan 1) (pr2 := derivable_pt_ps_atan x x_encad). - rewrite pr_nu_var2_interv with (f:=atan) (g:=atan) (lb:=-1) (ub:= 1) (pr2:=derivable_pt_atan x). + assert (Temp := derivable_pt_lim_ps_atan x x_encad). assert (Hrew1 : derive_pt ps_atan x (derivable_pt_ps_atan x x_encad) = (/(1 + x^2))). { apply derive_pt_eq_0 ; assumption. } rewrite derive_pt_atan. rewrite Hrew1. replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring). unfold Rdiv; rewrite Rmult_1_l; reflexivity. + lra. + assumption. + intros; reflexivity. - lra. - assert (t := tan_1_gt_1); split;destruct x_encad; lra. - intros; reflexivity. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia