data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n : ℕ}
--------
→ zero ≤ n
s≤s : ∀ {m n : ℕ}
→ m ≤ n
-------------
→ suc m ≤ suc n
infix 4 _≤_
≤-trans : ∀ {m n p : ℕ}
→ m ≤ n
→ n ≤ p
-----
→ m ≤ p
≤-trans z≤n _ = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)
≤-≡-trans : ∀ {m n p : ℕ}
→ m ≡ n
→ n ≤ p
-----
→ m ≤ p
≤-≡-trans refl z≤n = z≤n
≤-≡-trans refl (s≤s n≤p) = s≤s (≤-≡-trans refl n≤p)
module ≤-Reasoning where
infix 1 begin'_
infixr 2 step-≤-∣ step-≤-⟩ step-≤-≡-⟩
infix 3 _∎'
begin'_ : ∀ {x y : ℕ} → x ≤ y → x ≤ y
begin' x≤y = x≤y
step-≤-∣ : ∀ (x : ℕ) {y : ℕ} → x ≤ y → x ≤ y
step-≤-∣ x x≤y = x≤y
step-≤-⟩ : ∀ (x : ℕ) {y z : ℕ} → y ≤ z → x ≤ y → x ≤ z
step-≤-⟩ x y≤z x≤y = ≤-trans x≤y y≤z
step-≤-≡-⟩ : ∀ (x : ℕ) {y z : ℕ} → y ≤ z → x ≡ y → x ≤ z
step-≤-≡-⟩ x y≤z x≡y = ≤-≡-trans x≡y y≤z
syntax step-≤-∣ x x≤y = x ≤⟨⟩ x≤y
syntax step-≤-⟩ x y≤z x≤y = x ≤⟨ x≤y ⟩ y≤z
syntax step-≤-≡-⟩ x y≤z x≡y = x ≡'⟨ x≡y ⟩ y≤z
_∎' : ∀ (x : ℕ) → x ≤ x
zero ∎' = z≤n
suc x ∎' = s≤s (x ∎')
open ≤-Reasoning
+-monoˡ-≤ : (x y z : ℕ) → x ≤ y → x + z ≤ y + z
+-monoˡ-≤ x y zero x≤y =
begin'
x + zero
≡'⟨ +-identity x ⟩
x
≤⟨ x≤y ⟩
y
≡'⟨ sym (+-identity y) ⟩
y + zero
∎'
+-monoˡ-≤ x y (suc z) x≤y =
begin'
x + (suc z)
≡'⟨ +-comm x (suc z) ⟩
(suc z) + x
≡'⟨ refl ⟩
suc (z + x)
≡'⟨ cong suc (+-comm z x) ⟩
suc (x + z)
≤⟨ s≤s (+-monoˡ-≤ x y z x≤y) ⟩
suc (y + z)
≡'⟨ cong suc (+-comm y z) ⟩
suc (z + y)
≡'⟨ refl ⟩
(suc z) + y
≡'⟨ +-comm (suc z) y ⟩
y + (suc z)
∎'
+-monoʳ-≤ : (x y z : ℕ) → x ≤ y → z + x ≤ z + y
+-monoʳ-≤ x y zero x≤y = x≤y
+-monoʳ-≤ x y (suc z) x≤y =
begin'
suc (z + x)
≤⟨ s≤s (+-monoʳ-≤ x y z x≤y) ⟩
suc (z + y)
∎'
+-mono-≤ : ∀ (w x y z : ℕ) → w ≤ x → y ≤ z → w + y ≤ x + z
+-mono-≤ w x y z w≤x y≤z = ≤-trans (+-monoˡ-≤ w x y w≤x) (+-monoʳ-≤ y z x y≤z)