proposition: Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 -> -PI/2 < atan x - atan y < PI/2.
proof: Proof. assert (ut := PI_RGT_0). intros x y [xm1 x1] [ym1 y1]. assert (-(PI/4) <= atan x). { destruct xm1 as [xm1 | xm1]. { rewrite <- atan_1, <- atan_opp; apply Rlt_le, atan_increasing. assumption. } solve[rewrite <- xm1; change (-1) with (-(1)); rewrite atan_opp, atan_1; apply Rle_refl]. } assert (-(PI/4) < atan y). { rewrite <- atan_1, <- atan_opp; apply atan_increasing. assumption. } assert (atan x <= PI/4). { destruct x1 as [x1 | x1]. { rewrite <- atan_1; apply Rlt_le, atan_increasing. assumption. } solve[rewrite x1, atan_1; apply Rle_refl]. } assert (atan y < PI/4). { rewrite <- atan_1; apply atan_increasing. assumption. } rewrite Rdiv_opp_l; split; lra. Qed.
imports: Lia Lra Rbase Rtrigo1 Ranalysis_reg Rfunctions AltSeries Rseries SeqProp PartSum Ratan