diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-13 18:56:49 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-13 18:56:49 +0100 |
| commit | a90018e65444bcd7a4c85ddd815d315cd852e120 (patch) | |
| tree | f2941391474225246a2b8c04a8bd489d023dd801 /kvx/ExtFloats.v | |
| parent | d85683086bed8b76580616306166965079a02fb3 (diff) | |
| download | compcert-kvx-a90018e65444bcd7a4c85ddd815d315cd852e120.tar.gz compcert-kvx-a90018e65444bcd7a4c85ddd815d315cd852e120.zip | |
div_approx_reals_correct simplified proof
Diffstat (limited to 'kvx/ExtFloats.v')
| -rw-r--r-- | kvx/ExtFloats.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kvx/ExtFloats.v b/kvx/ExtFloats.v index f6dae39e..ea663735 100644 --- a/kvx/ExtFloats.v +++ b/kvx/ExtFloats.v @@ -70,7 +70,7 @@ Proof. apply Rabs_lt_inv in BALL. case (Rcompare_spec x (IZR y)); intro CMP. - left. apply Zfloor_imp. - replace (y-1+1) with y by ring. + ring_simplify (y-1+1). rewrite minus_IZR. lra. - subst. rewrite Zfloor_IZR. right. reflexivity. |