proposition: Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)).
proof: Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/3)); [ | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (2 * atan (/3) + atan (/7)) with (atan (/3) + (atan (/3) + atan (/7))) by ring. apply f_equal. replace (atan_sub 1 (/3)) with (/2) by (unfold atan_sub; field). rewrite (atan_sub_correct (/2) (/3)); [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. apply f_equal; unfold atan_sub; field. Qed.
imports: Lia Lra Rbase Rtrigo1 Ranalysis_reg Rfunctions AltSeries Rseries SeqProp PartSum Ratan