proposition: Lemma ArcTan_inv : forall x, ArcTan [--]x[=][--](ArcTan x).
proof: Proof. intros x. stepr (ArcTan [--](Tan (ArcTan x) (Dom_Tang_ArcTan x))). apply ArcTan_wd. apply un_op_wd_unfolded. apply Tan_ArcTan. assert (H:(olor ([--](Pi[/]TwoNZ)) (Pi[/]TwoNZ) [--](ArcTan x))). destruct (ArcTan_range x). split. apply inv_resp_less; assumption. rstepr ([--][--](Pi[/]TwoNZ)). apply inv_resp_less; assumption. stepr (ArcTan (Tan _ (Tang_Domain' _ H))). apply ArcTan_wd. apply eq_symmetric. apply Tan_inv. destruct H. apply ArcTan_Tan; assumption. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac