proposition: Lemma Rseq_setoid_theory : Setoid_Theory Rseq Rseq_eq.
proof: 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.
imports: Nnat Arith Ring Rsequence_def Reals Setoid