[add]: ≤-suc in Data.Nat.Properties

Author: pmbittner

src/Data/Nat/Properties.agda

@@ -171,6 +171,10 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≰⇒≥ {zero} {suc n} m≰n = contradiction z≤n m≰n
 ≰⇒≥ {suc m} {suc n} m≰n = s≤s (≰⇒≥ (m≰n ∘ s≤s))
 
+≤-suc : n ≤ m → n ≤ suc m
+≤-suc z≤n       = z≤n
+≤-suc (s≤s n≤m) = s≤s (≤-suc n≤m)
+
 ------------------------------------------------------------------------
 -- Relational properties of _≤_