path_fin_to_finnat_fin_zero@{} (n : nat) : fin_to_finnat (@fin_zero n) = zero_finnat n. Proof. apply path_sigma_hprop. apply path_nat_fin_zero. 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.