Require Import Reals.
Require Import Rsequence_def.

Delimit Scope RFseq_scope with Rseq.

Open Local Scope R_scope.
Open Local Scope RFseq_scope.

Implicit Type n : nat.
Implicit Type fn gn : nat → R → R.
Implicit Type f g : R → R.

Definition RFseq_plus fn gn n := (fn n + gn n)%F.
Definition RFseq_mult fn gn n := (fn n × gn n)%F.
Definition RFseq_opp fn n := (fun x ⇒ Ropp (fn n x))%F.
Definition RFseq_inv fn n := (fun x ⇒ Rinv (fn n x))%F.

Infix "+" := RFseq_plus : RFseq_scope.
Infix "×" := RFseq_mult : RFseq_scope.
Notation "- u" := (RFseq_opp u) : RFseq_scope.
Notation "/ u" := (RFseq_inv u) : RFseq_scope.

Definition RFseq_minus fn gn n := (fn n - gn n)%F.
Definition RFseq_div fn gn n := (fn n / gn n)%F.

Infix "-" := RFseq_minus : RFseq_scope.
Infix "/" := RFseq_div : RFseq_scope.

Definition RFseq_cv fn f := ∀ x, Rseq_cv (fun n ⇒ fn n x) (f x).
Definition RFseq_cv_interv fn f (lb ub : R) :=
  ∀ x, lb < x → x < ub → Rseq_cv (fun n ⇒ fn n x) (f x).

Definition RFseq_cvu fn f (x : R) (r : posreal) := ∀ eps : R, 0 < eps →
  ∃ N : nat, ∀ n (y : R), (N ≤ n)%nat → Boule x r y →
  R_dist (fn n y) (f y) < eps.