module My.SetTheory.Nat.Misc where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Data.Nat as DN
import Relation.Binary.PropositionalEquality as RBPE

open DN using (_+_)
open RBPE using (_≢_)

-- §──────────────────────────────────────────────────────────────────
-- Miscellany
-- §──────────────────────────────────────────────────────────────────

2+n≢1 : (n : DN.ℕ)  2 + n  1
2+n≢1 n ()