From a90018e65444bcd7a4c85ddd815d315cd852e120 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 13 Dec 2021 18:56:49 +0100 Subject: div_approx_reals_correct simplified proof --- kvx/ExtFloats.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kvx/ExtFloats.v') 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. -- cgit