Inequality1

Description

There is a useful syntax sugar for equality to rewriting contexts. But not for inequality (as far as I know). How can we rewriting inequality?

Theorem (download)

module Theorem where

open import Data.Nat

postulate
  m+n≤o→m≤o∸n : ∀ m n o → m + n ≤ o → m ≤ o ∸ n

Verifier

module Verifier where

open import Data.Nat
open import Theorem

verify : ∀ m n o → m + n ≤ o → m ≤ o ∸ n
verify = m+n≤o→m≤o∸n

Proofs

Rank Prover Size Date
1 trigott 272 2015-05-05 16:45:12 JST
2 notogawa 292 2013-09-01 21:38:59 JST
3 Lost_dog_ 713 2013-08-31 10:54:32 JST