proposition: Lemma arctan_explicit_Rball : Rball_eq 0 1 arctan arctan_sum.
proof: Proof. intros x x_in ; unfold arctan, arctan_pos, arctan_sum. destruct (Rlt_le_dec x 0). destruct (Rlt_le_dec (- x) 0). apply False_ind ; lra. destruct (Rle_lt_dec (- x) 1). destruct (Req_dec (- x) 1). destruct (Req_dec x 1). apply False_ind ; lra. apply False_ind ; destruct (Rabs_def2 _ _ x_in) ; lra. destruct (Req_dec x 1). apply False_ind ; lra. symmetry ; apply sum_r_arctan_odd ; assumption. apply False_ind ; destruct (Rabs_def2 _ _ x_in) ; lra. destruct (Rle_lt_dec x 1). reflexivity. apply False_ind ; destruct (Rabs_def2 _ _ x_in) ; lra. Qed.
imports: Rbase Rtactic Lra Ranalysis Rfunctions Rtrigo_facts Rseries_def SeqProp Rextensionality Rpser_usual RIVT Rseries_facts Rsequence_cv_facts MyRIneq Tactics Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis5