diff options
| -rw-r--r-- | lib/IEEE754_extra.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index d9329960..28da42ee 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -1066,6 +1066,16 @@ Proof. rewrite <- minus_IZR. apply IZR_lt. lia. + ** apply Rcompare_Eq. + assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra]. + field_simplify; [idtac | lra]. + rewrite <- mult_IZR. + rewrite <- mult_IZR. + rewrite <- mult_IZR. + rewrite <- plus_IZR. + rewrite <- minus_IZR. + replace (q * p2p + (q + 1) * p2p - 2 * zm) with 0 by lia. + field. lra. * symmetry. apply Znearest_imp with (n := zm / p2p). apply Rabs_lt. split. |