proposition: Lemma path_fin_to_finnat_fin_zero (n : nat) : fin_to_finnat (@fin_zero n) = zero_finnat n.
proof: Proof. apply path_sigma_hprop. apply path_nat_fin_zero. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin