path_finnat_to_fin_last@{} (n : nat) : finnat_to_fin (last_finnat n) = fin_last. Proof. induction n as [| n IHn]. - reflexivity. - exact (ap fsucc IHn). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoids Require Import Types.Empty Types.Sigma Types.Sum Types.Prod Types.Equiv. Require Import Spaces.Nat.Core. Require Import Finite.Fin.