Inequality1 by notogawa

module Theorem where

open import Data.Nat
open import Data.Nat.Properties
import Algebra
open Algebra.CommutativeSemiring commutativeSemiring using (+-comm)

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 with ≤′⇒≤ (≤′-refl {n})
... | n≤n with ∸-mono m+n≤o n≤n
... | m+n∸n≤o∸n
  rewrite +-∸-assoc m n≤n
        | n∸n≡0 n
        | +-comm m 0
        = m+n∸n≤o∸n