proposition: Lemma sinc_0 : sinc 0 = 1%R.
proof: Proof. unfold sinc. case exist_sin. simpl. unfold sin_in. intros y Hy. apply uniqueness_sum with (1 := Hy). intros eps He. exists 1. intros n Hn. rewrite (tech2 _ 0) by easy. simpl sum_f_R0 at 1. rewrite sum_eq_R0. unfold R_dist, sin_n. simpl. replace (1 / 1 * 1 + 0 - 1)%R with 0%R by field. now rewrite Rabs_R0. clear. intros m _. rewrite Rsqr_0, pow_i. apply Rmult_0_r. apply Nat.lt_0_succ. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)