proposition: Lemma path_finnat_to_fin_last (n : nat) : finnat_to_fin (last_finnat n) = fin_last.
proof: Proof. induction n as [| n IHn]. - reflexivity. - exact (ap fsucc IHn). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin