proposition: Lemma Cos_HalfPi : Cos (Pi [/]TwoNZ) [=] [0].
proof: Proof. transitivity (Cos (Lim (Build_CauchySeq _ _ pi_seq_Cauchy))). apply Cos_wd; unfold Pi in |- *; rational. astepr (Lim (Build_CauchySeq _ _ pi_seq_Cauchy) [-] Lim (Build_CauchySeq _ _ pi_seq_Cauchy)). assert (H : Cauchy_prop (fun n : nat => pi_seq (S n))). apply conv_seq_imp_conv_subseq with pi_seq S; auto with arith. intro; exists (S n); split; apply Nat.lt_succ_diag_r. simpl in |- *; auto. algebra. apply pi_seq_Cauchy. transitivity (Lim (Build_CauchySeq _ _ H) [-]Lim (Build_CauchySeq _ _ pi_seq_Cauchy)). 2: apply cg_minus_wd; algebra. 2: apply Lim_subseq_eq_Lim_seq with S; auto with arith. 2: intro; exists (S n); split; apply Nat.lt_succ_diag_r. 2: simpl in |- *; auto. 2: algebra. 2: left; intros; simpl in |- *. 2: apply local_mon_imp_mon'; auto; apply pi_seq_incr. eapply eq_transitive. 2: apply Lim_minus. assert (H0 : Cauchy_prop (fun n : nat => Cosine (pi_seq n) (cos_domain _))). apply Cauchy_prop_wd with (fun n : nat => pi_seq (S n) [-]pi_seq n). 2: intros; simpl in |- *; rational. exact (Cauchy_minus (Build_CauchySeq _ _ H) (Build_CauchySeq _ _ pi_seq_Cauchy)). transitivity (Lim (Build_CauchySeq _ _ H0)). 2: apply Lim_wd'; intros; simpl in |- *; rational. simpl in |- *. apply Continuous_imp_comm_Lim with (e := OneR) (x := Build_CauchySeq _ _ pi_seq_Cauchy) (Hxn := fun n : nat => cos_domain (pi_seq n)). apply pos_one. apply Included_imp_Continuous with realline; Contin. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos