proposition: Lemma Tan_ArcTan : forall (x : IR) Hx, x [=] Tan (ArcTan x) Hx.
proof: Proof. intros. set (y := Tan (ArcTan x) Hx) in *. assert (H : ArcTan x [=] ArcTan y). unfold y in |- *; apply eq_symmetric_unfolded; elim ArcTan_range with x; intros; apply ArcTan_Tan; auto. Transparent ArcTang. cut (Continuous_I (Min_leEq_Max x y) {1/} ( [-C-][1]{+}FId{^}2)). intro H0. cut (Integral H0 [=] [0]). intro H1. elim Hx; intros H2 H3. apply Integral_eq_zero with (contF := H0) (x := x). exact (pair (Min_leEq_lft x y) (lft_leEq_Max x y)). intros. simpl in |- *; apply recip_resp_pos. astepl (ZeroR[+][0]); apply plus_resp_less_leEq. apply pos_one. astepr (x[^]2); apply sqr_nonneg. intros x0 H4 Hx0; simpl in |- *. apply less_leEq; apply recip_resp_pos. astepl (ZeroR[+][0]); apply plus_resp_less_leEq. apply pos_one. astepr (x0[^]2); apply sqr_nonneg. auto. apply eq_transitive_unfolded with (ArcTan y[-]ArcTan x). rstepl (ArcTan x[+]Integral H0[-]ArcTan x). apply cg_minus_wd; [ simpl in |- * | algebra ]. apply eq_symmetric_unfolded; unfold ArcTan in |- *; simpl in |- *. apply Integral_plus_Integral with (Min3_leEq_Max3 [0] y x). apply included_imp_Continuous with realline. exact ArcTan_def_lemma. apply included3_interval; split. apply x_minus_x; simpl in |- *; algebra. apply included_imp_Continuous with realline. exact ArcTan_def_lemma. apply included_interval; split. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT