[ fixed #1484 ] prove m<n⇒m≤1+n by composition ≤-step ∘ <⇒≤ (#1485)

The pattern matching proof is a bit awkward (as the property is, which
combines two steps of information loss).

Author: andreasabel

src/Data/Nat/Properties.agda

@@ -418,8 +418,7 @@ m<n⇒n≢0 : ∀ {m n} → m < n → n ≢ 0
 m<n⇒n≢0 (s≤s m≤n) ()
 
 m<n⇒m≤1+n : ∀ {m n} → m < n → m ≤ suc n
-m<n⇒m≤1+n (s≤s z≤n)       = z≤n
-m<n⇒m≤1+n (s≤s (s≤s m<n)) = s≤s (m<n⇒m≤1+n (s≤s m<n))
+m<n⇒m≤1+n = ≤-step ∘ <⇒≤
 
 ∀[m≤n⇒m≢o]⇒n<o : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
 ∀[m≤n⇒m≢o]⇒n<o _       zero    m≤n⇒n≢0 = contradiction refl (m≤n⇒n≢0 z≤n)