proposition: Lemma arctan_explicit_pos : forall x, 1 <= x -> arctan x = 2 * arctan 1 - arctan_sum (/ x).
proof: Proof. intros x x_lb ; unfold arctan, arctan_sum, arctan_pos. destruct (Rlt_le_dec x 0). apply False_ind ; lra. destruct (Rle_lt_dec x 1). destruct (Rlt_le_dec 1 0). apply False_ind ; lra. destruct (Rle_lt_dec 1 1). destruct (Req_dec (/ x) 1) as [Heq | Hneq]. assert (Hx : x = 1). rewrite <- (Rmult_1_r x), <- Heq, Rinv_r. symmetry ; assumption. apply Rgt_not_eq ; lra. rewrite Hx, arctan_sum_1_PI4 ; ring. assert (Hx : x = 1) by (apply Rle_antisym ; assumption). apply False_ind, Hneq ; rewrite Hx, Rinv_1 ; reflexivity. apply False_ind ; lra. destruct (Rlt_le_dec 1 0). apply False_ind ; lra. destruct (Rle_lt_dec 1 1). unfold arctan_sum ; destruct (Req_dec (/ x) 1) as [Heq | Hneq]. assert (Hx : x = 1). rewrite <- (Rmult_1_r x), <- Heq, Rinv_r. symmetry ; assumption. apply Rgt_not_eq ; lra. apply False_ind ; lra. reflexivity. apply False_ind ; 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