proposition: Lemma ArcTan_plus_ArcTan : forall x y Hxy, ([--][1][<=]x) -> (x[<=][1]) -> ([--][1][<=]y) -> (y[<=][1]) -> ArcTan x [+] ArcTan y [=] ArcTan ((x[+]y)[/]([1][-]x[*]y)[//]Hxy).
proof: Proof. cut (forall x y Hxy, ([--][1][<=]x) -> (x[<=][1]) -> ([--][1][<=]y) -> (y[<][1]) -> ArcTan x [+] ArcTan y [=] ArcTan ((x[+]y)[/]([1][-]x[*]y)[//]Hxy)). intros G x y Hxy Hx0 Hx1 Hy0 Hy1. apply (not_ap_imp_eq). intros H. apply (leEq_less_or_equal _ _ _ Hx1). intros Hx1'. apply (leEq_less_or_equal _ _ _ Hy1). intros Hy1'. generalize H; clear H. apply (eq_imp_not_ap). clear Hy1. destruct Hy1' as [Hy1|Hy1]. apply G; assumption. assert (Hxy':([1][-]y[*]x)[#][0]). rstepl ([1][-]x[*]y). assumption. rstepl (ArcTan y[+]ArcTan x). stepr (ArcTan ((y[+]x)[/]([1][-]y[*]x)[//]Hxy')); [| now apply ArcTan_wd; rational]. apply G; try assumption. stepl ([1]:IR); [| now apply eq_symmetric; assumption]. apply leEq_reflexive. destruct Hx1' as [c|c]; try assumption. exfalso. refine (eq_imp_not_ap _ _ _ _ Hxy'). unfold cg_minus. csetoid_rewrite c. csetoid_rewrite Hy1. rstepl ([0]:IR). apply eq_reflexive. cut (forall x y Hxy, ([--][1][<=]x) -> (x[<=][1]) -> ([--][1][<]y) -> (y[<][1]) -> ArcTan x [+] ArcTan y [=] ArcTan ((x[+]y)[/]([1][-]x[*]y)[//]Hxy)). intros G x y Hxy Hx0 Hx1 Hy0 Hy1. apply (not_ap_imp_eq). intros H. apply (leEq_less_or_equal _ _ _ Hx0). intros Hx0'. apply (leEq_less_or_equal _ _ _ Hx1). intros Hx1'. apply (leEq_less_or_equal _ _ _ Hy0). intros Hy0'. generalize H; clear H. apply (eq_imp_not_ap). clear Hy0. destruct Hy0' as [Hy0|Hy0]. apply G; assumption. assert (Hxy':([1][-]y[*]x)[#][0]). rstepl ([1][-]x[*]y). assumption. destruct Hx0' as [Hx0'|Hx0']; destruct Hx1' as [Hx1'|Hx1']. rstepl (ArcTan y[+]ArcTan x). stepr (ArcTan ((y[+]x)[/]([1][-]y[*]x)[//]Hxy')); [| now apply ArcTan_wd; rational]. apply G; try assumption. stepr ([--][1]:IR); [| easy ]. apply leEq_reflexive. stepl ([--][1]:IR); [| easy ]. apply shift_zero_leEq_minus'. rstepr (Two:IR). apply less_leEq; apply pos_two. csetoid_replace (ArcTan y) ([--](ArcTan x)). rstepl ([0]:IR). stepl (ArcTan [0]); [| now apply ArcTan_zero]. apply ArcTan_wd. rstepl ([0][/]([1][-]x[*]y)[//]Hxy). apply div_wd. csetoid_rewrite Hx1'. csetoid_rewrite_rev Hy0. rational. apply eq_reflexive. stepl (ArcTan ([--]x)). apply ArcTan_inv. apply ArcTan_wd. csetoid_rewrite Hx1'. assumption. exfalso. refine (eq_imp_not_ap _ _ _ _ Hxy'). unfold cg_minus. csetoid_rewrite_rev Hx0'. csetoid_rewrite_rev Hy0. rational. exfalso. refine (eq_imp_not_ap _ [--][1] [1] _ _). 1: now stepr x. apply ap_symmetric. apply zero_minus_apart. rstepl (Two:IR). apply two_ap_zero. intros x y Hxy Hx0 Hx1 Hy0 Hy1. assert (X:olor [--](Pi [/]TwoNZ) (Pi [/]TwoNZ) (ArcTan x[+]ArcTan y)). split. rstepl ([--](Pi[/]FourNZ)[+][--](Pi[/]FourNZ)). csetoid_rewrite_rev (ArcTan_one). csetoid_replace ([--](ArcTan [1])) (ArcTan ([--][1])). apply plus_resp_leEq_less. apply ArcTan_resp_leEq; assumption. apply ArcTan_resp_less; assumption. apply eq_symmetric; apply ArcTan_inv. rstepr ((Pi[/]FourNZ)[+](Pi[/]FourNZ)). csetoid_rewrite_rev (ArcTan_one). apply plus_resp_leEq_less. apply ArcTan_resp_leEq; assumption. apply ArcTan_resp_less; assumption. elim X; intros X0 X1. csetoid_rewrite_rev (ArcTan_Tan _ X0 X1 (Tang_Domain' _ X)). apply ArcTan_wd. assert (Y:([1][-]Tan _ (Dom_Tang_ArcTan x)[*]Tan _ (Dom_Tang_ArcTan y))[#][0]). unfold cg_minus. csetoid_rewrite_rev (Tan_ArcTan _ (Dom_Tang_ArcTan x)). csetoid_rewrite_rev (Tan_ArcTan _ (Dom_Tang_ArcTan y)). assumption. stepr (Tan _ (Dom_Tang_ArcTan x)[+]Tan _ (Dom_Tang_ArcTan y)[/]_[//]Y). apply Tan_plus. apply div_wd; unfold cg_minus; csetoid_rewrite_rev (Tan_ArcTan _ (Dom_Tang_ArcTan x)); csetoid_rewrite_rev (Tan_ArcTan _ (Dom_Tang_ArcTan y)); apply eq_reflexive. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac