renaming: DivMod.nonZeroDivisor

Author: jamesmckinna

CHANGELOG.md

@@ -50,7 +50,7 @@ Additions to existing modules
   m/n≡0⇒m<n    : .{{_ : NonZero n}} → m / n ≡ 0 → m < n
   m/n≢0⇒n≤m    : .{{_ : NonZero n}} → m / n ≢ 0 → n ≤ m
 
-  nonZero      : DivMod dividend divisor → NonZero divisor
+  nonZeroDivisor : DivMod dividend divisor → NonZero divisor
   ```
 
 * Added new proofs in `Data.Nat.Properties`:
@@ -61,4 +61,4 @@ Additions to existing modules
   pred-cancel-< : pred m < pred n → m < n
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
-  ```
+  ```

src/Data/Nat/DivMod.agda

@@ -12,7 +12,7 @@ open import Agda.Builtin.Nat using (div-helper; mod-helper)
 
 open import Data.Fin.Base using (Fin; toℕ; fromℕ<)
 open import Data.Fin.Properties using (nonZeroIndex; toℕ-fromℕ<)
-open import Data.Nat.Base as Nat hiding (nonZero)
+open import Data.Nat.Base
 open import Data.Nat.DivMod.Core
 open import Data.Nat.Divisibility.Core
 open import Data.Nat.Induction
@@ -471,8 +471,8 @@ record DivMod (dividend divisor : ℕ) : Set where
     remainder : Fin divisor
     property  : dividend ≡ toℕ remainder + quotient * divisor
 
-  nonZero : NonZero divisor
-  nonZero = nonZeroIndex remainder
+  nonZeroDivisor : NonZero divisor
+  nonZeroDivisor = nonZeroIndex remainder
 
 
 infixl 7 _div_ _mod_ _divMod_