proposition: Lemma path_fin_to_finnat_fsucc {n : nat} (k : Fin n) : fin_to_finnat (fsucc k) = succ_finnat (fin_to_finnat k).
proof: Proof. apply path_sigma_hprop. apply path_nat_fsucc. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin