proposition: Lemma atan_inv : forall x, (0 < x)%R -> atan (/ x) = (PI / 2 - atan x)%R.
proof: Proof. intros x Hx. apply tan_inj. - apply atan_bound. - split. + apply Rlt_trans with R0. * unfold Rdiv. rewrite Ropp_mult_distr_l_reverse. apply Ropp_lt_gt_0_contravar. apply PI2_RGT_0. * apply Rgt_minus. apply atan_bound. + apply Rplus_lt_reg_r with (atan x - PI / 2)%R. ring_simplify. rewrite <- atan_0. now apply atan_increasing. - rewrite tan_atan. unfold tan. rewrite sin_shift. rewrite cos_shift. rewrite <- Rinv_div. apply f_equal, sym_eq, tan_atan. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia