proposition: Lemma atan_increasing : forall x y, x < y -> atan x < atan y.
proof: Proof. intros x y d. assert (t1 := atan_bound x). assert (t2 := atan_bound y). destruct (Rlt_le_dec (atan x) (atan y)) as [lt | bad]. { assumption. } apply Rlt_not_le in d. case d. rewrite <- (tan_atan y), <- (tan_atan x). destruct bad as [ylt | yx]. { apply Rlt_le, tan_increasing; try tauto. } solve[rewrite yx; apply Rle_refl]. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia