How to define function that finds the corresponding Field?

I tried to define function “sum (x y z: R): R := radd x (radd y z)” which finds the corresponding field structure. How to do it correctly - so that I don’t have to supply addition to it?

Thank you!

Set Implicit Arguments.

Require Import Field Equivalence Morphisms.
Section M.

  Variable R: Type.
  Variable req: R -> R -> Prop.

  Variable rEquiv: Equivalence req.

  Variables rO rI: R.
  Variable radd rmul rsub rdiv: R -> R -> R.
  Variable ropp rinv: R -> R.
  Variable Proper_radd: Proper (req ==> req ==> req) radd.
  Variable Proper_rmul: Proper (req ==> req ==> req) rmul.
  Variable Proper_rsub: Proper (req ==> req ==> req) rsub.
  Variable Proper_rdiv: Proper (req ==> req ==> req) rdiv.
  Variable Proper_ropp: Proper (req ==> req) ropp.
  Variable Proper_rinv: Proper (req ==> req) rinv.

  Variable field: field_theory rO rI radd rmul rsub ropp rdiv rinv req.
  Add Field Rfield: field.

  Definition sum (x y z: R): R := radd x (radd y z).

End M.

Require Import Reals.

Print sum.
Eval compute in sum Rplus (INR 1) (INR 2) (INR 3).