proposition: Lemma ArcTan_recip : forall x Hx, [0][<]x -> ArcTan ([1][/]x[//]Hx)[=]Pi[/]TwoNZ[-](ArcTan x).
proof: Proof. intros x Hx Hx0. assert (H0:olor [--](Pi [/]TwoNZ) (Pi [/]TwoNZ) ([--](ArcTan x)[+]Pi[/]TwoNZ)). split. apply shift_less_plus. rstepl ([--]Pi). apply inv_resp_less. apply less_transitive_unfolded with (Pi[/]TwoNZ). destruct (ArcTan_range x); assumption. auto with *. apply shift_plus_less. rstepr ([--][0]:IR). apply inv_resp_less. apply ArcTan_pos. assumption. rstepr ([--](ArcTan x)[+]Pi[/]TwoNZ). stepr (ArcTan (Tan _ (Tang_Domain' _ H0))); [| now destruct H0; apply ArcTan_Tan; assumption]. apply ArcTan_wd. apply eq_symmetric. assert (H1:Dom Tang ([--](ArcTan x))). apply Tang_Domain'. destruct (ArcTan_range x). split. apply inv_resp_less; assumption. rstepr ([--][--](Pi[/]TwoNZ)). apply inv_resp_less. assumption. assert (H2:(Tan [--](ArcTan x) H1)[#][0]). stepl ([--](Tan (ArcTan x) (Dom_Tang_ArcTan x))); [| now apply eq_symmetric; apply Tan_inv]. rstepr ([--][0]:IR). apply inv_resp_ap. apply Greater_imp_ap. csetoid_rewrite_rev (Tan_ArcTan x (Dom_Tang_ArcTan x)). assumption. eapply eq_transitive. apply (Tan_plus_HalfPi _ (Tang_Domain' _ H0) H1 H2). apply mult_cancel_lft with (Tan [--](ArcTan x) H1). assumption. apply mult_cancel_lft with x. apply Greater_imp_ap; assumption. rstepl ([--]x:IR). rstepr (Tan [--](ArcTan x) H1). stepr ([--](Tan (ArcTan x) (Dom_Tang_ArcTan x))). apply un_op_wd_unfolded. apply Tan_ArcTan. apply eq_symmetric. apply Tan_inv. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac