proposition: Lemma ArcTan_plus_ArcTan_Q : forall x y, -(1) <= x <= 1 -> -(1) <= y <= 1 -> ~1-x*y==0 -> (ArcTan (inj_Q _ x)[+]ArcTan (inj_Q _ y)[=]ArcTan (inj_Q _ (f x y))).
proof: Proof. intros x y [Hx0 Hx1] [Hy0 Hy1] H. assert (X:forall z, -(1) <= z -> [--][1][<=]inj_Q IR z). intros z Hz. stepl ((inj_Q IR (-(1)))). apply inj_Q_leEq; assumption. eapply eq_transitive. apply (inj_Q_inv IR (1)). apply un_op_wd_unfolded. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). assert (X0:forall z, z <= 1 -> inj_Q IR z[<=][1]). intros z Hz. stepr ((inj_Q IR ((1)))). apply inj_Q_leEq; assumption. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). assert ([1][-](inj_Q IR x)[*](inj_Q IR y)[#][0]). stepl (inj_Q IR (1[-]x[*]y)). (stepr (inj_Q IR [0]); [| now apply (inj_Q_nring IR 0)]). apply inj_Q_ap; assumption. eapply eq_transitive. apply inj_Q_minus. apply bin_op_wd_unfolded. rstepr (nring 1:IR); apply (inj_Q_nring IR 1). apply un_op_wd_unfolded. apply inj_Q_mult. apply eq_transitive with (ArcTan (inj_Q IR x[+]inj_Q IR y[/]([1][-]inj_Q IR x[*]inj_Q IR y)[//]X1)). apply ArcTan_plus_ArcTan; first [apply X; assumption |apply X0; assumption]. apply ArcTan_wd. stepl (inj_Q IR ((x[+]y)/([1][-]x*y))). apply inj_Q_wd. simpl. symmetry. apply f_char. assert (H0:(inj_Q IR ([1][-]x * y))[#][0]). (stepr (inj_Q IR 0); [| now apply (inj_Q_nring IR 0)]). apply inj_Q_ap; assumption. apply eq_transitive with (inj_Q IR (x[+]y)[/]inj_Q IR ([1][-]x * y)[//]H0). apply (inj_Q_div). apply div_wd. apply inj_Q_plus. eapply eq_transitive. apply inj_Q_minus. apply bin_op_wd_unfolded. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). apply un_op_wd_unfolded. apply inj_Q_mult. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.Q_in_CReals CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRarctan_small CoRN.transc.MoreArcTan CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q