[Add] Division properties for Nat, Integer, and Rational

src/Data/Integer/DivMod.agda

@@ -8,16 +8,23 @@
 
 module Data.Integer.DivMod where
 
-open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; NonZero; _%_; ∣_∣;
-  _%ℕ_; _/ℕ_; _+_; _*_; -_; _-_; pred; -1ℤ; 0ℤ; _⊖_; _≤_; _<_; +≤+; suc;
-  +<+)
+open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; ∣_∣; _+_; _*_; -_;
+  _-_; suc; pred; -1ℤ; 0ℤ; _⊖_; _≤_; _≥_; _<_; +≤+; -≤-; -≤+; +<+; -<+;
+  NonZero; NonNegative; NonPositive; Negative; Positive; sign;
+  nonNegative)
 open import Data.Integer.Properties
 open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; z<s; s<s)
-import Data.Nat.Properties as ℕ using (m∸n≤m)
-import Data.Nat.DivMod as ℕ using (m≡m%n+[m/n]*n; m%n≤n; m%n<n)
+import Data.Nat.Properties as ℕ using (≤-reflexive; m∸n≤m; m<n⇒0<n)
+import Data.Nat.DivMod as ℕ using (m≡m%n+[m/n]*n; m%n≤n; m%n<n; n/1≡n; n%1≡0;
+  m/n≡0⇒m<n; m<n⇒m/n≡0; sn%d≡0⇒sn/d≡s[n/d]; sn%d>0⇒sn/d≡n/d; /-monoˡ-≤;
+  /-monoʳ-≤; 0/n≡0)
+open import Data.Sign.Base using (opposite)
 open import Function.Base using (_∘′_)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; cong; sym; subst)
+open import Relation.Binary.Definitions using (Monotonic₁)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; cong; sym; subst; trans; refl)
+open import Relation.Nullary.Negation.Core using (contradiction)
+
 open ≤-Reasoning
 
 ------------------------------------------------------------------------
@@ -94,6 +101,20 @@ div-neg-is-neg-/ℕ n (ℕ.suc d) = -1*i≡-i (n /ℕ ℕ.suc d)
   rewrite div-pos-is-/ℕ n d {{d≢0}}
         = 0≤n⇒0≤n/ℕd n d 0≤n
 
+sn%d≡0⇒-[1+n]/ℕd≡-[1+n/d] : ∀ n d .{{_ : ℕ.NonZero d}} →
+                            ℕ.suc n ℕ.% d ≡ 0 → -[1+ n ] /ℕ d ≡ -[1+ n ℕ./ d ]
+sn%d≡0⇒-[1+n]/ℕd≡-[1+n/d] n d _ with ℕ.zero ← ℕ.suc n ℕ.% d in sn%d≡0 =
+  cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d sn%d≡0)
+
+n<0⇒n/ℕd<0 : ∀ n d .{{_ : ℕ.NonZero d}} → n < 0ℤ → (n /ℕ d) < 0ℤ
+n<0⇒n/ℕd<0 -[1+ n ] d -<+
+  with ℕ.suc n ℕ.% d | sn%d≡0⇒-[1+n]/ℕd≡-[1+n/d] n d
+... | ℕ.zero  | eq = begin-strict
+  - (+ (ℕ.suc n ℕ./ d)) ≡⟨ eq refl ⟩
+  -[1+ n ℕ./ d ]        <⟨ -<+ ⟩
+  + 0 ∎
+... | ℕ.suc _ | _ = -<+
+
 [n/d]*d≤n : ∀ n d .{{_ : NonZero d}} → (n / d) * d ≤ n
 [n/d]*d≤n n (+ d) = begin
   n / + d * + d        ≡⟨ cong (_* (+ d)) (div-pos-is-/ℕ n d) ⟩
@@ -129,6 +150,188 @@ a≡a%n+[a/n]*n n d@(-[1+ _ ]) = begin-equality
   + r + - q * d      ≡⟨ cong (_+_ (+ r) ∘′ (_* d)) (sym (-1*i≡-i q)) ⟩
   + r + n / d * d    ∎
 
+0/ℕd≡0 : ∀ d .{{_ : ℕ.NonZero d}} → + 0 /ℕ d ≡ + 0
+0/ℕd≡0 d = cong (+_) (ℕ.0/n≡0 d)
+
+0/d≡0 : ∀ d .{{_ : NonZero d}} → + 0 / d ≡ + 0
+0/d≡0 (+ d) = trans (div-pos-is-/ℕ (+ 0) d) (0/ℕd≡0 d)
+0/d≡0 -[1+ d ] = trans (div-neg-is-neg-/ℕ (+ 0) (ℕ.suc d))
+                       (cong (-_) (0/ℕd≡0 (ℕ.suc d)))
+
+n/ℕ1≡n : ∀ n → n /ℕ 1 ≡ n
+n/ℕ1≡n (+ n) = cong +_ (ℕ.n/1≡n n)
+n/ℕ1≡n -[1+ n ] rewrite ℕ.n%1≡0 (ℕ.suc n) = cong (-_ ∘′ +_) (ℕ.n/1≡n (ℕ.suc n))
+
+n/1≡n : ∀ n → n / + 1 ≡ n
+n/1≡n n = trans (div-pos-is-/ℕ n 1) (n/ℕ1≡n n)
+
+n/ℕd≡0⇒∣n∣<d : ∀ n d .{{_ : ℕ.NonZero d}} → n /ℕ d ≡ 0ℤ → ∣ n ∣ ℕ.< d
+n/ℕd≡0⇒∣n∣<d (+ n) d _ with ℕ.zero ← n ℕ./ d in n/d≡0 = ℕ.m/n≡0⇒m<n n/d≡0
+n/ℕd≡0⇒∣n∣<d (-[1+ n ]) d n/ℕd≡0 with ℕ.zero ← ℕ.suc n ℕ.% d
+    | ℕ.suc n ℕ./ d in n/d
+... | ℕ.zero  = ℕ.m/n≡0⇒m<n n/d
+... | ℕ.suc _ = contradiction n/ℕd≡0 λ ()
+
+n/d≡0⇒n<∣d∣ : ∀ n d .{{_ : NonZero d}} → n / d ≡ 0ℤ → n < + ∣ d ∣
+n/d≡0⇒n<∣d∣ n d@(+ d') n/d≡0ℤ = begin-strict
+  n ≤⟨ i≤∣i∣ n ⟩
+  + ∣ n ∣ <⟨ +<+ (n/ℕd≡0⇒∣n∣<d n d' n/ℕ∣d∣≡0) ⟩
+  + ∣ d ∣ ∎
+  where n/ℕ∣d∣≡0 = trans (sym (div-pos-is-/ℕ n d')) n/d≡0ℤ
+n/d≡0⇒n<∣d∣ n d@(-[1+ d' ]) n/d≡0ℤ = begin-strict
+  n ≤⟨ i≤∣i∣ n ⟩
+  + ∣ n ∣ <⟨ +<+ (n/ℕd≡0⇒∣n∣<d n (ℕ.suc d') n/ℕ∣d∣≡0) ⟩
+  + ∣ d ∣ ∎
+  where n/ℕ∣d∣≡0 = neg-injective (trans (sym (div-neg-is-neg-/ℕ n (ℕ.suc d'))) n/d≡0ℤ)
+
+n/d≡0⇒nonNeg-n : ∀ n d .{{_ : NonZero d}} → n / d ≡ 0ℤ → NonNegative n
+n/d≡0⇒nonNeg-n n d n/d≡0ℤ = nonNegative (begin
+  0ℤ ≡⟨ *-zeroˡ d ⟨
+  0ℤ * d ≡⟨ cong (_* d) n/d≡0ℤ ⟨
+  (n / d) * d ≤⟨ [n/d]*d≤n n d ⟩
+  n ∎)
+
+0≤n<d⇒n/ℕd≡0 : ∀ n d .{{_ : NonNegative n }} .{{_ : ℕ.NonZero d}} →
+                n < + d → n /ℕ d ≡ 0ℤ
+0≤n<d⇒n/ℕd≡0 (+ n) d (+<+ n<d) = cong (+_) (ℕ.m<n⇒m/n≡0 n<d)
+
+
+0≤n<∣d∣⇒n/d≡0 : ∀ n d .{{_ : NonNegative n }} .{{_ : NonZero d}} →
+                n < + ∣ d ∣ → n / d ≡ 0ℤ
+0≤n<∣d∣⇒n/d≡0 n (+ d) (+<+ n<d) = begin-equality
+  n / + d ≡⟨ div-pos-is-/ℕ n d ⟩
+  n /ℕ d  ≡⟨ (0≤n<d⇒n/ℕd≡0 n d (+<+ n<d)) ⟩
+  0ℤ ∎
+0≤n<∣d∣⇒n/d≡0 n -[1+ d ] (+<+ n<d) = begin-equality
+  n / -[1+ d ]     ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d) ⟩
+  - (n /ℕ ℕ.suc d) ≡⟨ cong (-_) (0≤n<d⇒n/ℕd≡0 n (ℕ.suc d) (+<+ n<d)) ⟩
+  - 0ℤ ∎
+
+private
+  /ℕ-monoˡ-≤-pos-pos : ∀ n m d .{{_ : NonNegative n}} .{{_ : NonNegative m}}
+                       .{{_ : ℕ.NonZero d}} → n ≤ m → n /ℕ d ≤ m /ℕ d
+  /ℕ-monoˡ-≤-pos-pos _ _ d (+≤+ n≤m) = +≤+ (ℕ./-monoˡ-≤ d n≤m)
+
+  /ℕ-monoˡ-≤-neg-pos : ∀ n m d .{{_ : Negative n}} .{{_ : NonNegative m}}
+                       .{{_ : ℕ.NonZero d}} → n ≤ m → n /ℕ d ≤ m /ℕ d
+  /ℕ-monoˡ-≤-neg-pos n@(-[1+ _ ]) m@(+ _) d -≤+ =
+    <⇒≤ (<-≤-trans (n<0⇒n/ℕd<0 n d -<+) (0≤n⇒0≤n/ℕd m d (+≤+ z≤n)))
+
+  n≡sk>0 : ∀ {n k} → n ≡ ℕ.suc k → 0 ℕ.< n
+  n≡sk>0 n≡sk = ℕ.m<n⇒0<n (ℕ.≤-reflexive (sym n≡sk))
+
+  /ℕ-monoˡ-≤-neg-neg : ∀ n m d .{{_ : Negative n}} .{{_ : Negative m}}
+                       .{{_ : ℕ.NonZero d}} → n ≤ m → n /ℕ d ≤ m /ℕ d
+  /ℕ-monoˡ-≤-neg-neg (-[1+ n ]) (-[1+ m ]) d (-≤- m≤n)
+    with ℕ.suc n ℕ.% d in sn%d | ℕ.suc m ℕ.% d in sm%d
+  ... | ℕ.zero | ℕ.zero  = neg-mono-≤ (+≤+ (ℕ./-monoˡ-≤ d (s≤s m≤n)))
+  ... | ℕ.zero | ℕ.suc _ = let sm%d>0 = n≡sk>0 sm%d in begin
+    -(+(ℕ.suc n ℕ./ d))   ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d sn%d) ⟩
+    -[1+ n ℕ./ d ]        ≤⟨ -≤- (ℕ./-monoˡ-≤ d m≤n) ⟩
+    -[1+ m ℕ./ d ]        ≡⟨ cong -[1+_] (ℕ.sn%d>0⇒sn/d≡n/d m d sm%d>0)⟨
+    -[1+ ℕ.suc m ℕ./ d ]  ∎
+  ... | ℕ.suc _ | ℕ.zero  = let sn%d>0 = n≡sk>0 sn%d in begin
+    -[1+ ℕ.suc n ℕ./ d ]  ≡⟨ cong -[1+_] (ℕ.sn%d>0⇒sn/d≡n/d n d sn%d>0)⟩
+    -[1+ n ℕ./ d ]        ≤⟨ -≤- (ℕ./-monoˡ-≤ d m≤n) ⟩
+    -(+(ℕ.suc (m ℕ./ d))) ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] m d sm%d) ⟨
+    -(+(ℕ.suc m ℕ./ d))   ∎
+  ... | ℕ.suc _ | ℕ.suc _ = -≤- (ℕ./-monoˡ-≤ d (s≤s m≤n))
+
+/ℕ-monoˡ-≤ : ∀ d .{{_ : ℕ.NonZero d}} → Monotonic₁ _≤_ _≤_ (_/ℕ d)
+/ℕ-monoˡ-≤ d {n@(+ _)}      {m@(+ _)}      n≤m = /ℕ-monoˡ-≤-pos-pos n m d n≤m
+/ℕ-monoˡ-≤ d {n@(-[1+ _ ])} {m@(+ _)}      n≤m = /ℕ-monoˡ-≤-neg-pos n m d n≤m
+/ℕ-monoˡ-≤ d {n@(-[1+ _ ])} {m@(-[1+ _ ])} n≤m = /ℕ-monoˡ-≤-neg-neg n m d n≤m
+
+/ℕ-monoʳ-≤-nonNeg : ∀ n {d₁ d₂} .{{_ : ℕ.NonZero d₁}} .{{_ : ℕ.NonZero d₂}}
+                    .{{_ : NonNegative n}} → d₁ ℕ.≤ d₂ → n /ℕ d₂ ≤ n /ℕ d₁
+/ℕ-monoʳ-≤-nonNeg (+ n) {d₁} {d₂} d₁≤d₂ = +≤+ (ℕ./-monoʳ-≤ n d₁≤d₂)
+
+/ℕ-monoʳ-≤-nonPos : ∀ n {d₁ d₂} .{{_ : ℕ.NonZero d₁}} .{{_ : ℕ.NonZero d₂}}
+                    .{{_ : NonPositive n}} → d₁ ℕ.≤ d₂ → n /ℕ d₁ ≤ n /ℕ d₂
+/ℕ-monoʳ-≤-nonPos (+ 0) {d₁} {d₂} d₁≤d₂ =
+  ≤-trans (≤-reflexive (0/ℕd≡0 d₁)) (≤-reflexive (sym (0/ℕd≡0 d₂)))
+/ℕ-monoʳ-≤-nonPos -[1+ n ] {d₁} {d₂} d₁≤d₂
+  with ℕ.suc n ℕ.% d₁ in sn%d₁ | ℕ.suc n ℕ.% d₂ in sn%d₂
+... | ℕ.zero | ℕ.zero  = neg-mono-≤ (+≤+ (ℕ./-monoʳ-≤ (ℕ.suc n) d₁≤d₂))
+... | ℕ.zero | ℕ.suc _ = let sn%d₂>0 = n≡sk>0 sn%d₂ in begin
+  -(+ (ℕ.suc n ℕ./ d₁)) ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d₁ sn%d₁) ⟩
+  -[1+ n ℕ./ d₁ ]       ≤⟨ -≤- (ℕ./-monoʳ-≤ n d₁≤d₂) ⟩
+  -[1+ n ℕ./ d₂ ]       ≡⟨ cong -[1+_] (ℕ.sn%d>0⇒sn/d≡n/d n d₂ sn%d₂>0) ⟨
+  -[1+ ℕ.suc n ℕ./ d₂ ] ∎
+... | ℕ.suc _ | ℕ.zero  = let sn%d₁>0 = n≡sk>0 sn%d₁ in begin
+  -[1+ ℕ.suc n ℕ./ d₁ ]   ≡⟨ cong -[1+_] (ℕ.sn%d>0⇒sn/d≡n/d n d₁ sn%d₁>0) ⟩
+  -[1+ n ℕ./ d₁ ]         ≤⟨ -≤- (ℕ./-monoʳ-≤ n d₁≤d₂) ⟩
+  -(+ (ℕ.suc (n ℕ./ d₂))) ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d₂ sn%d₂)⟨
+  -(+ (ℕ.suc n ℕ./ d₂))   ∎
+... | ℕ.suc _ | ℕ.suc _ = -≤- (ℕ./-monoʳ-≤ (ℕ.suc n) d₁≤d₂)
+
+/-monoˡ-≤-pos : ∀ d .{{_ : NonZero d}} .{{_ : Positive d}} →
+                Monotonic₁ _≤_ _≤_ (_/ d)
+/-monoˡ-≤-pos (+ d) {n} {m} n≤m = begin
+  n / (+ d) ≡⟨ div-pos-is-/ℕ n d ⟩
+  n /ℕ d    ≤⟨ /ℕ-monoˡ-≤ d n≤m ⟩
+  m /ℕ d    ≡⟨ div-pos-is-/ℕ m d ⟨
+  m / + d   ∎
+
+/-monoˡ-≤-neg : ∀ d .{{_ : NonZero d}} .{{_ : Negative d}} →
+                Monotonic₁ _≤_ _≥_ (_/ d)
+/-monoˡ-≤-neg -[1+ d ] {n} {m} n≤m = begin
+  m / -[1+ d ]     ≡⟨ div-neg-is-neg-/ℕ m (ℕ.suc d) ⟩
+  - (m /ℕ ℕ.suc d) ≤⟨ neg-mono-≤ (/ℕ-monoˡ-≤ (ℕ.suc d) n≤m) ⟩
+  - (n /ℕ ℕ.suc d) ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d) ⟨
+  n / - +[1+ d ]   ∎
+
+/-monoʳ-≤-nonNeg-eq-signs : ∀ n {d₁ d₂} .{{_ : NonZero d₁}} .{{_ : NonZero d₂}}
+                            .{{_ : NonNegative n}} → {sign d₁ ≡ sign d₂} →
+                            d₁ ≤ d₂ → n / d₁ ≥ n / d₂
+/-monoʳ-≤-nonNeg-eq-signs n {+ d₁} {+ d₂} (+≤+ d₁≤d₂) = begin
+  n / + d₂ ≡⟨ div-pos-is-/ℕ n d₂ ⟩
+  n /ℕ d₂  ≤⟨ /ℕ-monoʳ-≤-nonNeg n d₁≤d₂ ⟩
+  n /ℕ d₁  ≡⟨ div-pos-is-/ℕ n d₁ ⟨
+  n / + d₁ ∎
+/-monoʳ-≤-nonNeg-eq-signs n { -[1+ d₁ ] } { -[1+ d₂ ] } (-≤- d₂≤d₁) = begin
+  n / -[1+ d₂ ]     ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₂) ⟩
+  - (n /ℕ ℕ.suc d₂) ≤⟨ neg-mono-≤ (/ℕ-monoʳ-≤-nonNeg n (s≤s d₂≤d₁)) ⟩
+  - (n /ℕ ℕ.suc d₁) ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₁) ⟨
+  n / - +[1+ d₁ ]   ∎
+
+/-monoʳ-≤-nonPos-eq-signs : ∀ n {d₁ d₂} .{{_ : NonZero d₁}} .{{_ : NonZero d₂}}
+                            .{{_ : NonPositive n}} → {sign d₁ ≡ sign d₂} →
+                            d₁ ≤ d₂ → n / d₁ ≤ n / d₂
+/-monoʳ-≤-nonPos-eq-signs n {+ d₁} {+ d₂} (+≤+ d₁≤d₂) = begin
+  n / + d₁ ≡⟨ div-pos-is-/ℕ n d₁ ⟩
+  n /ℕ d₁  ≤⟨ /ℕ-monoʳ-≤-nonPos n d₁≤d₂ ⟩
+  n /ℕ d₂  ≡⟨ div-pos-is-/ℕ n d₂ ⟨
+  n / + d₂ ∎
+/-monoʳ-≤-nonPos-eq-signs n { -[1+ d₁ ] } { -[1+ d₂ ] } (-≤- d₂≤d₁) = begin
+  n / -[1+ d₁ ]     ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₁) ⟩
+  - (n /ℕ ℕ.suc d₁) ≤⟨ neg-mono-≤ (/ℕ-monoʳ-≤-nonPos n (s≤s d₂≤d₁)) ⟩
+  - (n /ℕ ℕ.suc d₂) ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₂) ⟨
+  n / - +[1+ d₂ ]   ∎
+
+/-monoʳ-≤-nonNeg-op-signs : ∀ n {d₁ d₂} .{{_ : NonZero d₁}} .{{_ : NonZero d₂}}
+                            .{{_ : NonNegative n}} →
+                            {sign d₁ ≡ opposite (sign d₂)} →
+                            d₁ ≤ d₂ → n / d₁ ≤ n / d₂
+/-monoʳ-≤-nonNeg-op-signs n { -[1+ d₁ ]} {+ d₂} -≤+ = begin
+  n / -[1+ d₁ ]     ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₁) ⟩
+  - (n /ℕ ℕ.suc d₁) ≤⟨ neg-mono-≤ (0≤n⇒0≤n/ℕd n (ℕ.suc d₁) (nonNegative⁻¹ n)) ⟩
+  0ℤ                ≤⟨ 0≤n⇒0≤n/d n (+ d₂) (nonNegative⁻¹ n) (+≤+ z≤n) ⟩
+  n / + d₂          ∎
+
+/-monoʳ-≤-nonPos-op-signs : ∀ n {d₁ d₂} .{{_ : NonZero d₁}} .{{_ : NonZero d₂}}
+                           .{{_ : NonPositive n}} →
+                           {sign d₁ ≡ opposite (sign d₂)} →
+                           d₁ ≤ d₂ → n / d₁ ≥ n / d₂
+/-monoʳ-≤-nonPos-op-signs (+ 0) {d₁@(-[1+ _ ])} {d₂@(+ _)} -≤+ =
+   ≤-trans (≤-reflexive (0/d≡0 d₂)) (≤-reflexive (sym (0/d≡0 d₁)))
+/-monoʳ-≤-nonPos-op-signs n@(-[1+ _ ]) { -[1+ d₁ ]} {+ d₂} -≤+ = begin
+  n / + d₂          ≡⟨ div-pos-is-/ℕ n d₂ ⟩
+  n /ℕ d₂           <⟨ n<0⇒n/ℕd<0 n d₂ (negative⁻¹ n) ⟩
+  0ℤ                <⟨ neg-mono-< (n<0⇒n/ℕd<0 n (ℕ.suc d₁) (negative⁻¹ n)) ⟩
+  - (n /ℕ ℕ.suc d₁) ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₁) ⟨
+  n / -[1+ d₁ ]     ∎
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Data/Integer/Properties.agda

@@ -728,6 +728,10 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒>
   ∣ i ∣ ℕ.+ ∣   j ∣        ∎
   where open ℕ.≤-Reasoning
 
+i≤∣i∣ : ∀ i → i ≤ + ∣ i ∣
+i≤∣i∣ (+ i) = ≤-reflexive (sym (0≤i⇒+∣i∣≡i (+≤+ z≤n)))
+i≤∣i∣ -[1+ i ] = -≤+
+
 ------------------------------------------------------------------------
 -- Properties of sign and _◃_
 

src/Data/Nat/DivMod.agda

@@ -125,6 +125,13 @@ m<[1+n%d]⇒m≤[n%d] {m} n (suc d-1) = k<1+a[modₕ]n⇒k≤a[modₕ]n 0 m n d-
 [1+m%d]≤1+n⇒[m%d]≤n : ∀ m n d .{{_ : NonZero d}} → 0 < suc m % d → suc m % d ≤ suc n → m % d ≤ n
 [1+m%d]≤1+n⇒[m%d]≤n m n (suc d-1) leq = 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 n m d-1 leq
 
+%-pred-≡suc : ∀ m d k .{{_ : NonZero d}} → suc m % d ≡ suc k → m % d ≡ k
+%-pred-≡suc m d k sm%d≡sk = ≤-antisym m%d≤k k≤m%d
+  where
+  k<sm%d = ≤-reflexive (sym sm%d≡sk)
+  m%d≤k = ([1+m%d]≤1+n⇒[m%d]≤n m k d (m<n⇒0<n k<sm%d) (≤-reflexive sm%d≡sk))
+  k≤m%d = m<[1+n%d]⇒m≤[n%d] m d k<sm%d
+
 %-distribˡ-+ : ∀ m n d .{{_ : NonZero d}} → (m + n) % d ≡ ((m % d) + (n % d)) % d
 %-distribˡ-+ m n d@(suc d-1) = begin-equality
   (m + n)                         % d ≡⟨ cong (λ v → (v + n) % d) (m≡m%n+[m/n]*n m d) ⟩
@@ -302,6 +309,43 @@ m/n≡1+[m∸n]/n {m@(suc m-1)} {n@(suc n-1)} m≥n = begin-equality
   pred (1 + (m ∸ n) / n) ≡⟨ cong pred (m/n≡1+[m∸n]/n n≥m) ⟨
   pred (m / n)           ∎
 
+sn%d≡0⇒sn/d≡s[n/d] : ∀ n d .{{_ : NonZero d}} → suc n % d ≡ 0 →
+                     suc n / d ≡ suc (n / d)
+sn%d≡0⇒sn/d≡s[n/d] n d@(suc _) sn%d≡0 =
+  *-cancelʳ-≡ (suc n / d) (suc (n / d)) d (begin-equality
+    suc n / d * d           ≡⟨ sn≡[sn/d]*d ⟨
+    suc n                   ≡⟨ cong suc (m≡m%n+[m/n]*n n d) ⟩
+    suc (n % d) + n / d * d ≡⟨ cong (_+ n / d * d) s[n%d]≡d ⟩
+    d + n / d * d           ≡⟨ cong (_+ n / d * d) (*-identityˡ d) ⟨
+    1 * d + n / d * d       ≡⟨ *-distribʳ-+ d 1 (n / d) ⟨
+    (1 + n / d) * d ∎ )
+  where
+  sn≡[sn/d]*d = trans (m≡m%n+[m/n]*n (suc n) d)
+                      (cong (_+ suc n / d * d) sn%d≡0)
+  s[n%d]≡d = trans (cong suc (%-pred-≡0 sn%d≡0)) (∸-suc z≤n)
+
+sn%d>0⇒sn/d≡n/d : ∀ n d .{{_ : NonZero d}} →
+                  0 < suc n % d → suc n / d ≡ n / d
+sn%d>0⇒sn/d≡n/d n d 0<sn%d with suc k ← suc n % d in sn%d≡sk =
+  *-cancelʳ-≡ (suc n / d) (n / d) d (begin-equality
+    suc n / d * d
+      ≡⟨ [n/d]*d≡n∸n%d (suc n) d ⟩
+    suc n ∸ suc n % d
+      ≡⟨ cong (suc n ∸_) sn%d≡sk ⟩
+    suc n ∸ suc k
+      ≡⟨ cong (λ x → suc x ∸ suc k) (m≡m%n+[m/n]*n n d) ⟩
+    suc (n % d) + n / d * d ∸ suc k
+      ≡⟨ cong (λ x → suc x + n / d * d ∸ suc k) (%-pred-≡suc n d k sn%d≡sk) ⟩
+    suc k + n / d * d ∸ suc k
+      ≡⟨ m+n∸m≡n (suc k) (n / d * d) ⟩
+    n / d * d ∎)
+  where
+  [n/d]*d≡n∸n%d : ∀ n d .{{_ : NonZero d}} → (n / d) * d ≡ n ∸ n % d
+  [n/d]*d≡n∸n%d n d = sym (begin-equality
+    n ∸ n % d           ≡⟨ cong (n ∸_) (m%n≡m∸m/n*n n d) ⟩
+    n ∸ (n ∸ n / d * d) ≡⟨ m∸[m∸n]≡n (m/n*n≤m n d) ⟩
+    n / d * d           ∎)
+
 m∣n⇒o%n%m≡o%m : ∀ m n o .{{_ : NonZero m}} .{{_ : NonZero n}} → m ∣ n →
                 o % n % m ≡ o % m
 m∣n⇒o%n%m≡o%m m n@.(p * m) o (divides-refl p) = begin-equality
@@ -574,4 +618,3 @@ m divMod n = result (m / n) (m mod n) $ begin-equality
   m % n                + [m/n]*n  ≡⟨ cong (_+ [m/n]*n) (toℕ-fromℕ< [m%n]<n) ⟨
   toℕ (fromℕ< [m%n]<n) + [m/n]*n  ∎
   where [m/n]*n = m / n * n ; [m%n]<n = m%n<n m n
-