proposition: Lemma is_lim_sinc_0 : is_lim (fun x => sin x / x) 0 1.
proof: Proof. apply is_lim_spec. move => eps. case: (derivable_pt_lim_sin_0 eps (cond_pos eps)) => delta H. exists delta => y Hy Hy0. rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= in Hy. rewrite /= -/(Rminus _ _) Rminus_0_r in Hy. move: (H y Hy0 Hy). by rewrite Rplus_0_l sin_0 Rminus_0_r. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis