Library Coq.Reals.Rtrigo_reg


Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo1.
Require Import Ranalysis1.
Require Import PSeries_reg.
Require Import Lra.
Local Open Scope nat_scope.
Local Open Scope R_scope.

Lemma continuity_sin : continuity sin.

Lemma CVN_R_sin :
  forall fn:nat -> R -> R,
    fn =
    (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)) ->
    CVN_R fn.

(sin h)/h -> 1 when h -> 0
((cos h)-1)/h -> 0 when h -> 0