Докажи м ≤ п -> к ≤ л -> т + к ≤ п + в Agda

Question

Я хочу доказать

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

в Agda. я могу доказать m + k ≤ m + l следующим кодом

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

Так как я могу доказать m + k ≤ m + l, я хочу доказать m + l ≤ n + l. Если я могу это сделать, я буду использовать ≤-trans : Transitive _≤_, который я уже определил.

Могу ли я доказать m + l ≤ n + l с m ≤ n, k ≤ l? Или, должен ли я изменить план использования ≤-trans?

Answer 1

Это просто

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)