Inequality1 by Lost_dog_

module Theorem where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
import Algebra
open Algebra.CommutativeSemiring commutativeSemiring using (+-comm; +-identity; +-assoc)
import Relation.Binary
open Relation.Binary.DecTotalOrder decTotalOrder using () renaming (trans to ≤-trans)


lem : ∀ n → pred n ≡ n ∸ 1
lem zero = refl
lem (suc n) = refl

m+n≤o→m≤o∸n : ∀ m n o → m + n ≤ o → m ≤ o ∸ n
m+n≤o→m≤o∸n m zero o m+n≤o rewrite proj₂ +-identity m = m+n≤o
m+n≤o→m≤o∸n m (suc n) o m+n≤o rewrite sym (+-assoc m 1 n) with m+n≤o→m≤o∸n (m + 1) n o m+n≤o
...| m+1≤o∸n with  m + 1 | +-comm m 1
...| .(1 + m) | refl with pred-mono m+1≤o∸n
...| m≤o∸n∸1 with pred (o ∸ n) | lem (o ∸ n)
...| .(o ∸ n ∸ 1) | refl with o ∸ n ∸ 1 | ∸-+-assoc o n 1
...| .(o ∸ (n + 1)) | refl with n + 1 | +-comm n 1
...| .(1 + n) | refl = m≤o∸n∸1