diff --git a/src/Core/Fcore_float_prop.v b/src/Core/Fcore_float_prop.v
index 077413bc9dec7a239f0e3ed8e98605db8a4d868a..a78ef6bfb0c8f29d7e9f21a86d0387070a8f4762 100644
--- a/src/Core/Fcore_float_prop.v
+++ b/src/Core/Fcore_float_prop.v
@@ -87,6 +87,15 @@ apply bpow_gt_0.
 now apply Z2R_lt.
 Qed.
 
+Theorem F2R_eq_compat :
+  forall e m1 m2 : Z,
+  (m1 = m2)%Z ->
+  (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.
+Proof.
+intros e m1 m2 H.
+now apply (f_equal (fun m => F2R (Float beta m e))).
+Qed.
+
 Theorem F2R_eq_reg :
   forall e m1 m2 : Z,
   F2R (Float beta m1 e) = F2R (Float beta m2 e) ->
diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v
index 8dfa2d7e70826ae27bfacc03c739697deb89618d..3da4ec3cc0791a8aeed59ffc9f712664511dc157 100644
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -341,7 +341,7 @@ intros (m, e) Hf.
 unfold canonic in Hf. simpl in Hf.
 unfold generic_format, scaled_mantissa.
 rewrite <- Hf.
-apply (f_equal (fun m => F2R (Float beta m e))).
+apply F2R_eq_compat.
 unfold F2R. simpl.
 rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
 now rewrite Ztrunc_Z2R.
@@ -710,7 +710,7 @@ Proof.
 intros x.
 unfold round.
 rewrite opp_F2R, canonic_exponent_opp, scaled_mantissa_opp.
-apply (f_equal (fun m => F2R (Float beta m _))).
+apply F2R_eq_compat.
 apply sym_eq.
 exact (Zopp_involutive _).
 Qed.
@@ -942,7 +942,7 @@ split ; intros Hx.
 (* *)
 replace (round rndZR x) with (round rndDN x).
 apply round_DN_pt.
-apply (f_equal (fun v => F2R (Float beta v _))).
+apply F2R_eq_compat.
 apply sym_eq.
 apply Ztrunc_floor.
 rewrite <- (Rmult_0_l (bpow (- canonic_exponent x))).
@@ -951,7 +951,7 @@ apply bpow_ge_0.
 (* *)
 replace (round rndZR x) with (round rndUP x).
 apply round_UP_pt.
-apply (f_equal (fun v => F2R (Float beta v _))).
+apply F2R_eq_compat.
 apply sym_eq.
 apply Ztrunc_ceil.
 rewrite <- (Rmult_0_l (bpow (- canonic_exponent x))).