proposition: Lemma cos_0 : cos 0 = 1.
proof: Proof. cut (cos_in 0 1). - cut (cos_in 0 (cos 0)). + apply uniqueness_sum. + rewrite <- Rsqr_0 at 1. exact (proj2_sig (exist_cos (Rsqr 0))). - unfold cos_in; unfold infinite_sum; intros; exists 0%nat. intros. unfold Rdist. induction n as [| n Hrecn]. + unfold cos_n; simpl. unfold Rdiv; rewrite Rinv_1. do 2 rewrite Rmult_1_r. unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + rewrite tech5. replace (cos_n (S n) * 0 ^ S n) with 0. * rewrite Rplus_0_r. apply Hrecn; unfold ge; apply Nat.le_0_l. * simpl; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia