FinNat.v

Require Import
  HoTT.Basics
  HoTT.Types
  HoTT.HSet
  HoTT.Spaces.Nat.Core
  HoTT.Spaces.Finite.Fin.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope nat_scope.

Definition FinNat (n : nat) : Type0 := {x : nat | x < n}.

Definition zero_finnat (n : nat) : FinNat n.+1
  := (0; leq_1_Sn).

Lemma path_zero_finnat (n : nat) (h : 0 < n.+1) : zero_finnat n = (0; h).n: nat
h: 0 < n.+1
zero_finnat n = (0; h)
Proof.n: nat
h: 0 < n.+1
zero_finnat n = (0; h)
  by apply path_sigma_hprop.
Defined.

Definition succ_finnat {n : nat} (u : FinNat n) : FinNat n.+1
  := (u.1.+1; leq_S_n' u.1.+1 n u.2).

Lemma path_succ_finnat {n : nat} (u : FinNat n) (h : u.1.+1 < n.+1)
  : succ_finnat u = (u.1.+1; h).n: nat
u: FinNat n
h: (u.1).+1 < n.+1
succ_finnat u = ((u.1).+1; h)
Proof.n: nat
u: FinNat n
h: (u.1).+1 < n.+1
succ_finnat u = ((u.1).+1; h)
  by apply path_sigma_hprop.
Defined.

Definition last_finnat (n : nat) : FinNat n.+1
  := exist (fun x => x < n.+1) n (leq_refl n.+1).

Lemma path_last_finnat (n : nat) (h : n < n.+1)
  : last_finnat n = (n; h).n: nat
h: n < n.+1
last_finnat n = (n; h)
Proof.n: nat
h: n < n.+1
last_finnat n = (n; h)
  by apply path_sigma_hprop.
Defined.

Definition incl_finnat {n : nat} (u : FinNat n) : FinNat n.+1
  := (u.1; leq_trans u.2 (leq_S n n (leq_n n))).

Lemma path_incl_finnat (n : nat) (u : FinNat n) (h : u.1 < n.+1)
  : incl_finnat u = (u.1; h).n: nat
u: FinNat n
h: u.1 < n.+1
incl_finnat u = (u.1; h)
Proof.n: nat
u: FinNat n
h: u.1 < n.+1
incl_finnat u = (u.1; h)
  by apply path_sigma_hprop.
Defined.

Definition finnat_ind (P : forall n : nat, FinNat n -> Type)
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
  {n : nat} (u : FinNat n)
  : P n u.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
P n u
Proof.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
P n u
  induction n as [| n IHn].P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
u: FinNat 0
P 0 u
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n.+1
IHn: forall u : FinNat n, P n u
P n.+1 u
  -P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
u: FinNat 0
P 0 u elim (not_lt_n_0 u.1 u.2).
  -P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n.+1
IHn: forall u : FinNat n, P n u
P n.+1 u destruct u as [x h].P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, x: nat
h: x < n.+1
IHn: forall u : FinNat n, P n u
P n.+1 (x; h)
    destruct x as [| x].P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
h: 0 < n.+1
IHn: forall u : FinNat n, P n u
P n.+1 (0; h)
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, P n u
P n.+1 (x.+1; h)
    +P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
h: 0 < n.+1
IHn: forall u : FinNat n, P n u
P n.+1 (0; h) exact (transport (P n.+1) (path_zero_finnat _ h) (z _)).
    +P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, P n u
P n.+1 (x.+1; h) refine (transport (P n.+1) (path_succ_finnat (x; leq_S_n _ _ h) _) _).P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, P n u
P n.+1 (succ_finnat (x; leq_S_n x.+1 n h))
      apply s.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, P n u
P n (x; leq_S_n x.+1 n h) apply IHn.
Defined.

Lemma compute_finnat_ind_zero (P : forall n : nat, FinNat n -> Type)
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
  (n : nat)
  : finnat_ind P z s (zero_finnat n) = z n.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
finnat_ind P z s (zero_finnat n) = z n
Proof.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
finnat_ind P z s (zero_finnat n) = z n
  cbn.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
transport (P n.+1) (path_zero_finnat n leq_1_Sn) (z n) =
z n by induction (hset_path2 1 (path_zero_finnat n leq_1_Sn)).
Defined.

Lemma compute_finnat_ind_succ (P : forall n : nat, FinNat n -> Type)
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n),
       P n u -> P n.+1 (succ_finnat u))
  {n : nat} (u : FinNat n)
  : finnat_ind P z s (succ_finnat u) = s n u (finnat_ind P z s u).P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
finnat_ind P z s (succ_finnat u) =
s n u (finnat_ind P z s u)
Proof.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
finnat_ind P z s (succ_finnat u) =
s n u (finnat_ind P z s u)
  refine
    (_ @ transport
          (fun p => transport _ p (s n u _) = s n u (finnat_ind P z s u))
          (hset_path2 1 (path_succ_finnat u (leq_S_n' _ _ u.2))) 1).P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
finnat_ind P z s (succ_finnat u) =
transport (P n.+1)
  (path_succ_finnat u (leq_S_n' (u.1).+1 n u.2))
  (s n u (finnat_ind P z s u))
  destruct u as [u1 u2].P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
finnat_ind P z s (succ_finnat (u1; u2)) =
transport (P n.+1)
  (path_succ_finnat (u1; u2)
     (leq_S_n' ((u1; u2).1).+1 n (u1; u2).2))
  (s n (u1; u2) (finnat_ind P z s (u1; u2)))
  assert (u2 = leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2)) as p.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
u2 = leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2)
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
p: u2 = leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2)
finnat_ind P z s (succ_finnat (u1; u2)) =
transport (P n.+1)
  (path_succ_finnat (u1; u2)
     (leq_S_n' ((u1; u2).1).+1 n (u1; u2).2))
  (s n (u1; u2) (finnat_ind P z s (u1; u2)))
  -P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
u2 = leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2) apply path_ishprop.
  -P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
p: u2 = leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2)
finnat_ind P z s (succ_finnat (u1; u2)) =
transport (P n.+1)
  (path_succ_finnat (u1; u2)
     (leq_S_n' ((u1; u2).1).+1 n (u1; u2).2))
  (s n (u1; u2) (finnat_ind P z s (u1; u2))) simpl.P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
p: u2 = leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2)
transport (P n.+1)
  (path_succ_finnat
     (u1; leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2))
     (leq_S_n' u1.+1 n u2))
  (s n (u1; leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2))
     (finnat_ind P z s
        (u1; leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2)))) =
transport (P n.+1)
  (path_succ_finnat (u1; u2) (leq_S_n' u1.+1 n u2))
  (s n (u1; u2) (finnat_ind P z s (u1; u2))) by induction p.
Defined.

Monomorphic Definition is_bounded_fin_to_nat {n} (k : Fin n)
  : fin_to_nat k < n.n: nat
k: Fin n
fin_to_nat k < n
Proof.n: nat
k: Fin n
fin_to_nat k < n
  induction n as [| n IHn].k: Fin 0
fin_to_nat k < 0
n: nat
k: Fin n.+1
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat k < n.+1
  -k: Fin 0
fin_to_nat k < 0 elim k.
  -n: nat
k: Fin n.+1
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat k < n.+1 destruct k as [k | []].n: nat
k: Fin n
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inl k) < n.+1
n: nat
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inr tt) < n.+1
    +n: nat
k: Fin n
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inl k) < n.+1 apply (@leq_trans _ n _).n: nat
k: Fin n
IHn: forall k : Fin n, fin_to_nat k < n
(fin_to_nat (inl k)).+1 <= n
n: nat
k: Fin n
IHn: forall k : Fin n, fin_to_nat k < n
n <= n.+1
      *n: nat
k: Fin n
IHn: forall k : Fin n, fin_to_nat k < n
(fin_to_nat (inl k)).+1 <= n apply IHn.
      *n: nat
k: Fin n
IHn: forall k : Fin n, fin_to_nat k < n
n <= n.+1 by apply leq_S.
    +n: nat
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inr tt) < n.+1 apply leq_refl.
Defined.

Monomorphic Definition fin_to_finnat {n} (k : Fin n) : FinNat n
  := (fin_to_nat k; is_bounded_fin_to_nat k).

Monomorphic Fixpoint finnat_to_fin {n : nat} : FinNat n -> Fin n
  := match n with
     | 0 => fun u => Empty_rec (not_lt_n_0 _ u.2)
     | n.+1 => fun u =>
        match u with
        | (0; _) => fin_zero
        | (x.+1; h) => fsucc (finnat_to_fin (x; leq_S_n _ _ h))
        end
     end.

Lemma path_fin_to_finnat_fsucc {n : nat} (k : Fin n)
  : fin_to_finnat (fsucc k) = succ_finnat (fin_to_finnat k).n: nat
k: Fin n
fin_to_finnat (fsucc k) =
succ_finnat (fin_to_finnat k)
Proof.n: nat
k: Fin n
fin_to_finnat (fsucc k) =
succ_finnat (fin_to_finnat k)
  apply path_sigma_hprop.n: nat
k: Fin n
(fin_to_finnat (fsucc k)).1 =
(succ_finnat (fin_to_finnat k)).1
  apply path_nat_fsucc.
Defined.

Lemma path_fin_to_finnat_fin_zero (n : nat)
  : fin_to_finnat (@fin_zero n) = zero_finnat n.n: nat
fin_to_finnat fin_zero = zero_finnat n
Proof.n: nat
fin_to_finnat fin_zero = zero_finnat n
  apply path_sigma_hprop.n: nat
(fin_to_finnat fin_zero).1 = (zero_finnat n).1
  apply path_nat_fin_zero.
Defined.

Lemma path_fin_to_finnat_fin_incl {n : nat} (k : Fin n)
  : fin_to_finnat (fin_incl k) = incl_finnat (fin_to_finnat k).n: nat
k: Fin n
fin_to_finnat (fin_incl k) =
incl_finnat (fin_to_finnat k)
Proof.n: nat
k: Fin n
fin_to_finnat (fin_incl k) =
incl_finnat (fin_to_finnat k)
  reflexivity.
Defined.

Lemma path_fin_to_finnat_fin_last (n : nat)
  : fin_to_finnat (@fin_last n) = last_finnat n.n: nat
fin_to_finnat fin_last = last_finnat n
Proof.n: nat
fin_to_finnat fin_last = last_finnat n
  reflexivity.
Defined.

Lemma path_finnat_to_fin_succ {n : nat} (u : FinNat n)
  : finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u).n: nat
u: FinNat n
finnat_to_fin (succ_finnat u) =
fsucc (finnat_to_fin u)
Proof.n: nat
u: FinNat n
finnat_to_fin (succ_finnat u) =
fsucc (finnat_to_fin u)
  cbn.n: nat
u: FinNat n
fsucc
  (finnat_to_fin
     (u.1;
     leq_rec (u.1).+2
       (fun m : nat => (u.1).+1 <= pred m)
       (leq_n (u.1).+1)
       (fun (m : nat) (H : (u.1).+2 <= m)
          (IHleq : (u.1).+1 <= pred m) =>
        match
          m as n
          return
            ((u.1).+2 <= n ->
             (u.1).+1 <= pred n -> (u.1).+1 <= n)
        with
        | 0 => fun _ : (u.1).+2 <= 0 => idmap
        | n.+1 =>
            fun (_ : (u.1).+2 <= n.+1)
              (IHleq0 : (u.1).+1 <= n) =>
            leq_S (u.1).+1 n IHleq0
        end H IHleq) n.+1 (leq_S_n' (u.1).+1 n u.2))) =
fsucc (finnat_to_fin u) do 2 f_ap.n: nat
u: FinNat n
(u.1;
leq_rec (u.1).+2 (fun m : nat => (u.1).+1 <= pred m)
  (leq_n (u.1).+1)
  (fun (m : nat) (H : (u.1).+2 <= m)
     (IHleq : (u.1).+1 <= pred m) =>
   match
     m as n
     return
       ((u.1).+2 <= n ->
        (u.1).+1 <= pred n -> (u.1).+1 <= n)
   with
   | 0 => fun _ : (u.1).+2 <= 0 => idmap
   | n.+1 =>
       fun (_ : (u.1).+2 <= n.+1)
         (IHleq0 : (u.1).+1 <= n) =>
       leq_S (u.1).+1 n IHleq0
   end H IHleq) n.+1 (leq_S_n' (u.1).+1 n u.2)) = u by apply path_sigma_hprop.
Defined.

Lemma path_finnat_to_fin_zero (n : nat)
  : finnat_to_fin (zero_finnat n) = fin_zero.n: nat
finnat_to_fin (zero_finnat n) = fin_zero
Proof.n: nat
finnat_to_fin (zero_finnat n) = fin_zero
  reflexivity.
Defined.

Lemma path_finnat_to_fin_incl {n : nat} (u : FinNat n)
  : finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u).n: nat
u: FinNat n
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
Proof.n: nat
u: FinNat n
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
  induction n as [| n IHn].u: FinNat 0
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
n: nat
u: FinNat n.+1
IHn: forall u : FinNat n,
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
  -u: FinNat 0
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u) elim (not_lt_n_0 _ u.2).
  -n: nat
u: FinNat n.+1
IHn: forall u : FinNat n,
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u) destruct u as [x h].n, x: nat
h: x < n.+1
IHn: forall u : FinNat n,
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
finnat_to_fin (incl_finnat (x; h)) =
fin_incl (finnat_to_fin (x; h))
    destruct x as [| x]; [reflexivity|].n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n,
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
finnat_to_fin (incl_finnat (x.+1; h)) =
fin_incl (finnat_to_fin (x.+1; h))
    refine ((ap _ (ap _ (path_succ_finnat (x; leq_S_n _ _ h) h)))^ @ _).n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n,
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
finnat_to_fin
  (incl_finnat (succ_finnat (x; leq_S_n x.+1 n h))) =
fin_incl (finnat_to_fin (x.+1; h))
    refine (_ @ ap fsucc (IHn (x; leq_S_n _ _ h))).n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n,
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
finnat_to_fin
  (incl_finnat (succ_finnat (x; leq_S_n x.+1 n h))) =
fsucc
  (finnat_to_fin (incl_finnat (x; leq_S_n x.+1 n h)))
    by induction (path_finnat_to_fin_succ (incl_finnat (x; leq_S_n _ _ h))).
Defined.

Lemma path_finnat_to_fin_last (n : nat)
  : finnat_to_fin (last_finnat n) = fin_last.n: nat
finnat_to_fin (last_finnat n) = fin_last
Proof.n: nat
finnat_to_fin (last_finnat n) = fin_last
  induction n as [| n IHn].finnat_to_fin (last_finnat 0) = fin_last
n: nat
IHn: finnat_to_fin (last_finnat n) = fin_last
finnat_to_fin (last_finnat n.+1) = fin_last
  -finnat_to_fin (last_finnat 0) = fin_last reflexivity.
  -n: nat
IHn: finnat_to_fin (last_finnat n) = fin_last
finnat_to_fin (last_finnat n.+1) = fin_last exact (ap fsucc IHn).
Defined.

Lemma path_finnat_to_fin_to_finnat {n : nat} (u : FinNat n)
  : fin_to_finnat (finnat_to_fin u) = u.n: nat
u: FinNat n
fin_to_finnat (finnat_to_fin u) = u
Proof.n: nat
u: FinNat n
fin_to_finnat (finnat_to_fin u) = u
  induction n as [| n IHn].u: FinNat 0
fin_to_finnat (finnat_to_fin u) = u
n: nat
u: FinNat n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
fin_to_finnat (finnat_to_fin u) = u
  -u: FinNat 0
fin_to_finnat (finnat_to_fin u) = u elim (not_lt_n_0 _ u.2).
  -n: nat
u: FinNat n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
fin_to_finnat (finnat_to_fin u) = u destruct u as [x h].n, x: nat
h: x < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
fin_to_finnat (finnat_to_fin (x; h)) = (x; h)
    apply path_sigma_hprop.n, x: nat
h: x < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x; h))).1 = (x; h).1
    destruct x as [| x].n: nat
h: 0 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (0; h))).1 = (0; h).1
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x.+1; h))).1 =
(x.+1; h).1
    +n: nat
h: 0 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (0; h))).1 = (0; h).1 exact (ap pr1 (path_fin_to_finnat_fin_zero n)).
    +n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x.+1; h))).1 =
(x.+1; h).1 refine ((path_fin_to_finnat_fsucc _)..1 @ _).n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(succ_finnat
   (fin_to_finnat
      ((fix finnat_to_fin (n : nat) :
            FinNat n -> Fin n :=
          match
            n as n0 return (FinNat n0 -> Fin n0)
          with
          | 0 =>
              fun u : FinNat 0 =>
              Empty_rec (not_lt_n_0 u.1 u.2)
          | n0.+1 =>
              fun u : FinNat n0.+1 =>
              let u0 := u in
              let proj1 := u0.1 in
              let h := u0.2 in
              match
                proj1 as proj2
                return (proj2 < n0.+1 -> Fin n0.+1)
              with
              | 0 => fun _ : 0 < n0.+1 => fin_zero
              | x.+1 =>
                  fun h0 : x.+1 < n0.+1 =>
                  fsucc
                    (finnat_to_fin n0
                       (x; leq_S_n x.+1 n0 h0))
              end h
          end) n (x; leq_S_n x.+1 n h)))).1 =
(x.+1; h).1
      exact (ap S (IHn (x; leq_S_n _ _ h))..1).
Defined.

Lemma path_fin_to_finnat_to_fin {n : nat} (k : Fin n)
  : finnat_to_fin (fin_to_finnat k) = k.n: nat
k: Fin n
finnat_to_fin (fin_to_finnat k) = k
Proof.n: nat
k: Fin n
finnat_to_fin (fin_to_finnat k) = k
  induction n as [| n IHn].k: Fin 0
finnat_to_fin (fin_to_finnat k) = k
n: nat
k: Fin n.+1
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat k) = k
  -k: Fin 0
finnat_to_fin (fin_to_finnat k) = k elim k.
  -n: nat
k: Fin n.+1
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat k) = k destruct k as [k | []].n: nat
k: Fin n
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inl k)) = inl k
n: nat
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inr tt)) = inr tt
    +n: nat
k: Fin n
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inl k)) = inl k specialize (IHn k).n: nat
k: Fin n
IHn: finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inl k)) = inl k
      refine (path_finnat_to_fin_incl (fin_to_finnat k) @ _).n: nat
k: Fin n
IHn: finnat_to_fin (fin_to_finnat k) = k
fin_incl (finnat_to_fin (fin_to_finnat k)) = inl k
      exact (ap fin_incl IHn).
    +n: nat
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inr tt)) = inr tt apply path_finnat_to_fin_last.
Defined.

Definition equiv_fin_finnat (n : nat) : Fin n <~> FinNat n
  := equiv_adjointify fin_to_finnat finnat_to_fin
      path_finnat_to_fin_to_finnat
      path_fin_to_finnat_to_fin.