proposition: Lemma Derivative_Tan_1 : forall H, Derivative (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) H Tang {1/} (Cosine{^}2).
proof: Proof. intros. assert (H0 : Derivative _ H Sine Cosine). apply Included_imp_Derivative with realline I; Deriv. assert (H1 : Derivative _ H Cosine {--}Sine). apply Included_imp_Derivative with realline I; Deriv. assert (H2 : forall x : IR, olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ) x -> Cos x [#] [0]). intros x H2; apply Greater_imp_ap; inversion_clear H2; apply Cos_pos; auto. unfold Tang in |- *. Derivative_Help. apply eq_imp_Feq. apply included_FDiv. apply included_FMinus; Included. Included. intros; simpl in |- *; apply ap_wdl with (Cos x[*]Cos x). apply mult_resp_ap_zero; auto. simpl in |- *; algebra. 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. intros x H3 Hx Hx'. apply eq_transitive_unfolded with (Cos x[*]Cos x[-]Sin x[*][--] (Sin x) [/] _[//] mult_resp_ap_zero _ _ _ (H2 x H3) (H2 x H3)). elim Hx; intros H4 H5. astepl (Part _ _ (ProjIR1 (H4, H5)) [/] _[//] ext2 (S:=IR) (ProjIR2 (H4, H5))). astepl (Part _ _ H4[/] _[//]ext2 (S:=IR) H5); clear Hx. apply div_wd. simpl in |- *. astepl (Part _ _ (ProjIR1 H4) [-]Part _ _ (ProjIR2 H4)). elim H4; clear H4; intros H6 H7. astepl (Part _ _ H6[-]Part _ _ H7). apply cg_minus_wd; simpl in |- *; algebra. elim H5; clear H5; intros H6 H7. astepl (Part _ _ H6). simpl in |- *; algebra. apply eq_transitive_unfolded with ([1][/] _[//]mult_resp_ap_zero _ _ _ (H2 x H3) (H2 x H3)). apply div_wd. 2: simpl in |- *; algebra. astepr (Cos x[^]2[+]Sin x[^]2); simpl in |- *; rational. simpl in Hx'; astepr ([1][/] _[//]ext2 (S:=IR) Hx'). apply div_wd. algebra. astepl ([1][*]Cos x[*]Cos x); simpl in |- *; algebra. apply Derivative_div. Deriv. Deriv. apply bnd_Cos. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac