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 ()