diff --git a/orders/rationals.v b/orders/rationals.v
index b8ad987a..055eb51b 100644
--- a/orders/rationals.v
+++ b/orders/rationals.v
@@ -34,6 +34,7 @@ Section rationals_and_another_rationals.
   Context `{Rationals Q2} `{Apart Q2} `{!TrivialApart Q2} `{!FullPseudoSemiRingOrder (A:=Q2) Q2le Q2lt}
      {f : Q1 → Q2} `{!SemiRing_Morphism f}.
 
+  Add Ring Q1 : (F_R (stdlib_field_theory Q1)).
   Add Field Q1 : (stdlib_field_theory Q1).
 
   Notation i_to_r := (integers.integers_to_ring (SRpair nat) Q1).
@@ -93,6 +94,7 @@ Instance rationals_lt  `{Rationals Q} : Lt Q | 10 := dec_lt.
 Section default_order.
   Context `{Rationals Q} `{Apart Q} `{!TrivialApart Q}.
 
+  Add Ring R: (F_R (stdlib_field_theory Q)).
   Add Field F: (stdlib_field_theory Q).
   Notation n_to_sr := (naturals_to_semiring nat Q).
 
diff --git a/theory/dec_fields.v b/theory/dec_fields.v
index 050281a2..7e59ad2a 100644
--- a/theory/dec_fields.v
+++ b/theory/dec_fields.v
@@ -205,6 +205,7 @@ Section from_stdlib_field_theory.
     `{!Proper (Fe ==> Fe) Fnegate}
     `{!Proper (Fe ==> Fe) Frecip}.
 
+  Add Ring F2 : (F_R ftheory).
   Add Field F2 : ftheory.
 
   Definition from_stdlib_field_theory: @DecField F Fe Fplus Fmult Fzero Fone Fnegate Frecip.
diff --git a/theory/int_pow.v b/theory/int_pow.v
index 28dde7ff..ba288b7f 100644
--- a/theory/int_pow.v
+++ b/theory/int_pow.v
@@ -10,6 +10,7 @@ Require Import
 Section int_pow_properties.
 Context `{DecField A} `{∀ x y, Decision (x = y)} `{Integers B} `{!IntPowSpec A B ipw}.
 
+Add Ring A : (F_R (dec_fields.stdlib_field_theory A)).
 Add Field A : (dec_fields.stdlib_field_theory A).
 Add Ring B : (rings.stdlib_ring_theory B).