proposition: Lemma Derivative_ArTanH : forall H, Derivative DomArTanH H ArTangH (Frecip ([-C-][1]{-}FId{^}2)).
proof: Proof. intros H. assert (bnd_away_zero_in_P ([-C-][1]{-}FId) DomArTanH). clear H. intros a b Hab H. split. Included. exists ([1][-]b). destruct (H _ (compact_inc_rht _ _ Hab)) as [_ A]. apply shift_zero_less_minus. assumption. intros y Hy H0. simpl. eapply leEq_transitive;[|apply leEq_AbsIR]. apply plus_resp_leEq_lft. apply inv_resp_leEq. destruct H0; assumption. unfold ArTangH. unfold Half. eapply Derivative_wdr; [|apply Derivative_scal; eapply (Derivative_comp DomArTanH (openl [0]) H I);[apply ArTanH_maps_compact_lemma | Derivative_Help; apply Feq_reflexive|Deriv]]. FEQ. apply included_FScalMult. apply included_FMult. apply included_FComp. Included. intros x Hx Hx0. split. repeat constructor. simpl; intros _. apply div_resp_ap_zero_rev. apply Greater_imp_ap. rstepr (x[-][--][1]). apply shift_zero_less_minus. destruct Hx0; assumption. apply included_FDiv. repeat constructor. repeat constructor. intros x Hx0 Hx. simpl. apply Greater_imp_ap. rstepr (([1][-]x)[^]2). apply pos_square. apply Greater_imp_ap. apply shift_zero_less_minus. destruct Hx0; assumption. apply included_FRecip. repeat constructor. intros x Hx0 Hx. simpl. rstepl (([1][-]x)[*](x[-][--][1])). apply Greater_imp_ap. apply mult_resp_pos; apply shift_zero_less_minus; destruct Hx0; assumption. apply included_FDiv. repeat constructor. repeat constructor. intros x H0 Hx. simpl. rstepl (([1][-]x)[^]2). apply Greater_imp_ap. apply pos_square. apply Greater_imp_ap. apply shift_zero_less_minus. destruct H0; assumption. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac