Prove m ≤ n -> k ≤ l -> m + k ≤ n + l in Agda

Question

I want to prove

{m n k l : ℕ} -> m ≤ n -> k ≤ l -> m + k ≤ n + l

in Agda. I can prove m + k ≤ m + l by the following code

add≤ : {m n : ℕ} -> (k : ℕ) -> m ≤ n -> k + m ≤ k + n
add≤ zero exp = exp
add≤ (suc k) exp = s≤s (add≤ k exp)

Since I can prove m + k ≤ m + l, I want to prove m + l ≤ n + l. If I can do that, I will use ≤-trans : Transitive _≤_ which I have already defined.

Can I prove m + l ≤ n + l with m ≤ n, k ≤ l? Or, Should I have to change the plan to use ≤-trans?

Answer 1

It's simply

open import Data.Nat
open import Data.Nat.Properties

le : {m n k l : ℕ} -> m ≤ n -> k ≤ l -> m + k ≤ n + l
le {n = n}  z≤n    q = ≤-steps n q
le         (s≤s p) q = s≤s (le p q)