diff --git a/Chain.agda b/Chain.agda
index b1778d4..8aaf247 100644
--- a/Chain.agda
+++ b/Chain.agda
@@ -7,8 +7,10 @@ module Chain {a} {A : Set a}
              (R-≈-cong : ∀ {a₁ a₁' a₂ a₂'} → a₁ ≈ a₁' → a₂ ≈ a₂' → a₁ R a₂ → a₁' R a₂') where
 
 open import Data.Nat as Nat using (ℕ; suc; _+_; _≤_)
+open import Data.Nat.Properties using (+-comm; m+1+n≰m)
 open import Data.Product using (_×_; Σ; _,_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+open import Data.Empty using (⊥)
 
 open IsEquivalence ≈-equiv
 
@@ -36,5 +38,11 @@ module _  where
     Bounded : ℕ → Set a
     Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound
 
+    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → ⊥
+    Bounded-suc-n {a₁} {a₂} {n} bounded c = (m+1+n≰m n n+1≤n)
+        where
+            n+1≤n : n + 1 ≤ n
+            n+1≤n rewrite (+-comm n 1) = bounded c
+
     Height : ℕ → Set a
     Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)