proposition: Lemma atan_def x : -(pi / 2) < atan x < pi / 2 /\ tan (atan x) = x.
proof: Proof. rewrite /atan; case: xgetP => //= He. pose x1 := Num.sqrt (1 + x^+ 2) ^-1. have ox2_gt0 : 0 < 1 + x^2. by apply: lt_le_trans (_ : 1 <= _); rewrite ?lerDl ?sqr_ge0. have ox2_ge0 : 0 <= 1 + x^2 by rewrite ltW. have x1B : -1 <= x1 <= 1. rewrite -ler_norml /x1 ger0_norm ?sqrtr_ge0 // -[leRHS]sqrtr1. by rewrite ler_psqrt ?qualifE/= ?invr_gte0 //= invf_cp1 // lerDl sqr_ge0. case: (He (Num.sg x * acos x1)); split; last first. case: (x =P 0) => [->|/eqP xD0]; first by rewrite /tan sgr0 mul0r sin0 mul0r. rewrite /tan sin_sg cos_sg // acosK ?sin_acos //. rewrite /x1 sqr_sqrtr// ?invr_ge0 //. rewrite -{1}[_^-1 in X in X / _ = _]mul1r. rewrite -{1}[X in X - _](divff (_: 1 != 0)) //. rewrite -mulNr addf_div ?lt0r_neq0 //. rewrite mul1r mulr1 [X in X - 1]addrC addrK // sqrtrM ?sqr_ge0 //. rewrite sqrtrV // invrK // mulrA divfK //; last by rewrite sqrtr_eq0 -ltNge. by rewrite sqrtr_sqr mulr_sg_norm. rewrite -ltr_norml normrM. have pi2 : 0 < pi / 2 :> R by rewrite divr_gt0 // pi_gt0. case: (x =P 0) => [->|/eqP xD0]; first by rewrite sgr0 normr0 mul0r. rewrite normr_sg xD0 mul1r ltr_norml. rewrite (@lt_le_trans _ _ 0) ?acos_ge0 ?oppr_cp0 //=. rewrite -ltr_cos ?in_itv/= ?acos_ge0/= ?acos_lepi//; last first. by rewrite divr_ge0 ?pi_ge0//= ler_pdivrMr// ler_pMr ?pi_gt0// ler1n. by rewrite cos_pihalf acosK // ?sqrtr_gt0 ?invr_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp