# Library Coqtail.Reals.Rsequence.Rsequence_ring

Require Import Nnat.

Require Import Arith.

Require Export Ring.

Require Import Rsequence_def.

Require Import Reals.

Require Import Setoid.

Open Scope Rseq_scope.

Add Morphism Rseq_plus with signature Rseq_eq ==> Rseq_eq ==> Rseq_eq as Rseq_plus_Rseq_eq_compat.

Proof.

unfold Rseq_eq, Rseq_plus.

intros Un Vn Huv Xn Yn Hxy n.

rewrite Huv.

rewrite Hxy.

reflexivity.

Qed.

Add Morphism Rseq_minus : Rseq_minus_Rseq_eq_compat.

Proof.

unfold Rseq_eq, Rseq_minus.

intros Un Vn Huv Xn Yn Hxy n.

rewrite Huv.

rewrite Hxy.

reflexivity.

Qed.

Add Morphism Rseq_mult with signature Rseq_eq ==> Rseq_eq ==> Rseq_eq as Rseq_mult_Rseq_eq_compat.

Proof.

unfold Rseq_eq, Rseq_mult.

intros Un Vn Huv Xn Yn Hxy n.

rewrite Huv.

rewrite Hxy.

reflexivity.

Qed.

Add Morphism Rseq_opp with signature Rseq_eq ==> Rseq_eq as Rseq_opp_Rseq_eq_compat.

Proof.

intros x y H i.

unfold Rseq_eq, Rseq_opp.

rewrite H.

trivial.

Qed.

Lemma Rseq_setoid_theory : Setoid_Theory Rseq Rseq_eq.

Proof.

constructor; unfold Rseq_eq.

unfold Reflexive; trivial.

unfold Symmetric; auto.

unfold Transitive; intros x y z H1 H2 n;

rewrite H1; rewrite H2; reflexivity.

Qed.

Lemma Rseq_ring_theory : @ring_theory Rseq (0%R) (1%R) Rseq_plus Rseq_mult Rseq_minus Rseq_opp Rseq_eq.

Proof.

constructor; unfold Rseq_plus, Rseq_mult, Rseq_minus, Rseq_eq, Rseq_constant, Rseq_opp;

intros; ring.

Qed.

Add Setoid Rseq Rseq_eq Rseq_setoid_theory as Rseq_eq_setoid.

Add Ring Rseq_Ring : Rseq_ring_theory(abstract).