proposition: Theorem Alt_PI_eq : Alt_PI = PI.
proof: Proof. apply Rmult_eq_reg_r with (/4); fold (Alt_PI/4); fold (PI/4); [ | apply Rgt_not_eq; lra]. assert (0 < PI/6) by (apply PI6_RGT_0). assert (t1:= PI2_1). assert (t2 := PI_4). assert (m := Alt_PI_RGT_0). assert (-PI/2 < 1 < PI/2) by (rewrite Rdiv_opp_l; split; lra). apply cond_eq; intros eps ep. change (Rdist (Alt_PI/4) (PI/4) < eps). assert (ca : continuity_pt atan 1). { apply derivable_continuous_pt, derivable_pt_atan. } assert (Xe : exists eps', exists eps'', eps' + eps'' <= eps /\ 0 < eps' /\ 0 < eps''). { exists (eps/2); exists (eps/2); repeat apply conj; lra. } destruct Xe as [eps' [eps'' [eps_ineq [ep' ep'']]]]. destruct (ps_atan_continuity_pt_1 _ ep') as [alpha [a0 Palpha]]. destruct (ca _ ep'') as [beta [b0 Pbeta]]. assert (Xa : exists a, 0 < a < 1 /\ Rdist a 1 < alpha /\ Rdist a 1 < beta). { exists (Rmax (/2) (Rmax (1 - alpha /2) (1 - beta /2))). assert (/2 <= Rmax (/2) (Rmax (1 - alpha /2) (1 - beta /2))) by apply Rmax_l. assert (Rmax (1 - alpha /2) (1 - beta /2) <= Rmax (/2) (Rmax (1 - alpha /2) (1 - beta /2))) by apply Rmax_r. assert ((1 - alpha /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_l. assert ((1 - beta /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_r. assert (Rmax (1 - alpha /2) (1 - beta /2) < 1) by (apply Rmax_lub_lt; lra). split;[split;[ | apply Rmax_lub_lt]; lra | ]. assert (0 <= 1 - Rmax (/ 2) (Rmax (1 - alpha / 2) (1 - beta / 2))). { assert (Rmax (/2) (Rmax (1 - alpha / 2) (1 - beta /2)) <= 1) by (apply Rmax_lub; lra). lra. } split; unfold Rdist; rewrite <-Rabs_Ropp, Ropp_minus_distr, Rabs_pos_eq;lra. } destruct Xa as [a [[Pa0 Pa1] [P1 P2]]]. apply Rle_lt_trans with (1 := Rdist_tri _ _ (ps_atan a)). apply Rlt_le_trans with (2 := eps_ineq). apply Rplus_lt_compat. { rewrite Rdist_sym; apply Palpha; assumption. } rewrite <- atan_eq_ps_atan. { rewrite <- atan_1; apply (Pbeta a); auto. split; [ | exact P2]. split;[exact I | apply Rgt_not_eq; assumption]. } split; assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia