module My.SetTheory.Fin.Misc where

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

import Data.Fin as DF
import Data.Nat as DN
import Function as F
import Relation.Binary.PropositionalEquality as RBPE

open F using (_$_)
open RBPE using (_≢_)

import My.SetTheory.Nat.TvD as MySTNTVD

-- §──────────────────────────────────────────────────────────────────
-- Basic properties.
-- §──────────────────────────────────────────────────────────────────

iFinN⇒N≢toℕi : {n : DN.ℕ} → (i : DF.Fin n) → n ≢ DF.toℕ i
iFinN⇒N≢toℕi {} () n≡toℕi
iFinN⇒N≢toℕi {DN.suc n} DF.zero ()
iFinN⇒N≢toℕi {DN.suc n} (DF.suc i) n≡toℕi =
  iFinN⇒N≢toℕi i $ MySTNTVD.sm≡sn⇒m≡n n≡toℕi