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).``````