proposition: Lemma Derivative_Tan_2 : forall H, Derivative (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) H Tang ( [-C-][1]{+}Tang{^}2).
proof: Proof. intros. eapply Derivative_wdr. 2: apply Derivative_Tan_1. assert (H0 : forall x : IR, olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ) x -> Cos x [#] [0]). intros x H0; apply Greater_imp_ap; inversion_clear H0; apply Cos_pos; auto. apply eq_imp_Feq. apply included_FRecip. Included. intros; simpl in |- *; apply ap_wdl with (Cos x[*]Cos x). apply mult_resp_ap_zero; auto. astepl ([1][*]Cos x[*]Cos x); simpl in |- *; algebra. apply included_FPlus. Included. apply included_FNth. unfold Tang in |- *; apply included_FDiv. Included. Included. intros; simpl in |- *; astepl (Cos x). algebra. simpl in |- *; algebra. intros x H1 Hx Hx'. apply eq_transitive_unfolded with ([1][/] _[//]mult_resp_ap_zero _ _ _ (H0 x H1) (H0 x H1)). simpl in |- *; apply div_wd. algebra. astepr ([1][*]Cos x[*]Cos x); simpl in |- *; algebra. astepl (Cos x[^]2[+]Sin x[^]2[/] _[//]mult_resp_ap_zero _ _ _ (H0 x H1) (H0 x H1)). apply eq_transitive_unfolded with ([1][+][1][*] (Sin x[/] _[//]H0 x H1) [*] (Sin x[/] _[//]H0 x H1)). 2: simpl in |- *; apply bin_op_wd_unfolded. 2: algebra. 2: repeat simple apply mult_wd; try apply div_wd; algebra. simpl in |- *. rational. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac