proposition: Lemma Machin_2_3 : PI/4 = atan(/2) + atan(/3).
proof: Proof. assert (utility : 0 < PI/2) by (apply PI2_RGT_0). rewrite <- atan_1. rewrite (atan_sub_correct 1 (/2)). - apply f_equal, f_equal; unfold atan_sub; field. - apply Rgt_not_eq; lra. - apply tech; try split; try lra. - apply atan_bound. Qed.
imports: Lia Lra Rbase Rtrigo1 Ranalysis_reg Rfunctions AltSeries Rseries SeqProp PartSum Ratan