\import Arith.Nat(pred)
\import Logic
\import Paths
\cons fzero {n : Nat} : Fin (suc n) => 0
\cons fsuc {n : Nat} (x : Fin n) : Fin (suc n) => suc x
\func fpred {n : Nat} (def : Fin n) (x : Fin (suc n)) : Fin n \elim x
| 0 => def
| suc x => x
\func fcase {A : \Type} {n : Nat} (a : A) (f : Fin n -> A) (j : Fin (suc n)) : A \elim j
| 0 => a
| suc j => f j
\lemma unfsuc {n : Nat} {x y : Fin n} (p : suc x = suc y) : x = y
=> pmap (fpred x) p
\lemma fsuc/= {n : Nat} {x y : Fin n} (p : x /= y) : fsuc x /= fsuc y
=> \lam q => p (unfsuc q)
\lemma fsuc/=0 {n : Nat} {x : Fin n} : fsuc x /= 0
=> \case __
\lemma fsuc/=-conv {n : Nat} {x y : Fin n} (p : fsuc x /= fsuc y) : x /= y
=> \lam q => p (pmap fsuc q)
\lemma nat_fin_= {n : Nat} {x y : Fin n} (p : x = {Nat} y) : x = y \elim n, x, y
| suc n, 0, 0 => idp
| suc n, 0, suc y => \case p
| suc n, suc x, 0 => \case p
| suc n, suc x, suc y => pmap fsuc (nat_fin_= (pmap pred p))
\lemma fin_nat_/= {n : Nat} {x y : Fin n} (p : x /= y) : (x : Nat) /= y
=> \lam q => p (nat_fin_= q)
\lemma fsuc_fpred {n : Nat} {x : Fin (suc n)} {d : Fin n} (p : x /= 0) : fsuc (fpred d x) = x \elim x
| 0 => absurd (p idp)
| suc x => idp
\func fpredP {n : Nat} (j : Fin (suc n)) (j/=0 : j /= 0) : Fin n \elim j
| 0 => absurd (j/=0 idp)
| suc j => j
\lemma fsuc_fpredP {n : Nat} {x : Fin (suc n)} (p : x /= 0) : fsuc (fpredP x p) = x \elim x
| 0 => absurd (p idp)
| suc x => idp
\func finLast (n : Nat) : Fin (suc n) \elim n
| 0 => 0
| suc n => suc (finLast n)