diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v
index 573ae3ca44ea0abaeee058c64ecda35d1d5b6d29..9cd62b8bf339bb8a16fc9215e65159524ecfe6c4 100644
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -552,6 +552,17 @@ Qed.
 
 End Fcore_generic_rounding_pos.
 
+Theorem rounding_ext :
+  forall rnd1 rnd2,
+  ( forall x e, Zrnd rnd1 x e = Zrnd rnd2 x e ) ->
+  forall x,
+  rounding rnd1 x = rounding rnd2 x.
+Proof.
+intros rnd1 rnd2 Hext x.
+unfold rounding.
+now rewrite Hext.
+Qed.
+
 Section Zrounding_opp.
 
 Variable rnd : Zrounding.