diff options
Diffstat (limited to 'theories/ZArith/Zdiv.v')
| -rw-r--r-- | theories/ZArith/Zdiv.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 27fb21bc7..32993b2c0 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -683,7 +683,7 @@ Arguments Zdiv_eucl_extended : default implicits. (** * Division and modulo in Z agree with same in nat: *) -Require Import NPeano. +Require Import PeanoNat. Lemma div_Zdiv (n m: nat): m <> O -> Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m. |