Inequality1 by trigott

module Theorem where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

m≤m : ∀ m → m ≤ m
m≤m zero    = z≤n
m≤m (suc m) = s≤s (m≤m m)

m+n≤o→m≤o∸n : ∀ m n o → m + n ≤ o → m ≤ o ∸ n
m+n≤o→m≤o∸n m n o m+n≤o = begin
  m
    ≡⟨ sym (m+n∸n≡m m n) ⟩
  m + n ∸ n
    ≤⟨ ∸-mono m+n≤o (m≤m n) ⟩
  o ∸ n
    ∎
  where open ≤-Reasoning