path_finnat_to_fin_to_finnat@{} {n : nat} (u : FinNat n) : fin_to_finnat (finnat_to_fin u) = u. Proof. induction n as [| n IHn]. - elim (not_lt_zero_r _ u.2). - destruct u as [x h]. apply path_sigma_hprop. destruct x as [| x]. + exact (ap pr1 (path_fin_to_finnat_fin_zero n)). + refine ((path_fin_to_finnat_fsucc _)..1 @ _). exact (ap S (IHn (x; leq_pred' h))..1). 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.