diff options
Diffstat (limited to 'flocq/Core/Raux.v')
| -rw-r--r-- | flocq/Core/Raux.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v index 455190dc..221d84d6 100644 --- a/flocq/Core/Raux.v +++ b/flocq/Core/Raux.v @@ -18,7 +18,7 @@ COPYING file for more details. *) (** * Missing definitions/lemmas *) -Require Export Psatz. +Require Import Psatz. Require Export Reals ZArith. Require Export Zaux. @@ -1277,7 +1277,7 @@ Theorem Zfloor_div : Zfloor (IZR x / IZR y) = (x / y)%Z. Proof. intros x y Zy. -generalize (Z_div_mod_eq_full x y Zy). +generalize (Z.div_mod x y Zy). intros Hx. rewrite Hx at 1. assert (Zy': IZR y <> 0%R). |