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 {0} () 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