agda - 在 Agda 中证明 m ≤ n -> k ≤ l -> m + k ≤ n + l

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)