proposition: Lemma path_finnat_to_fin_to_finnat {n : nat} (u : FinNat n) : fin_to_finnat (finnat_to_fin u) = u.
proof: Proof. induction n as [| n IHn]. - elim (not_lt_n_0 _ 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_S_n _ _ h))..1). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin