proposition: Lemma path_succ_finnat {n : nat} (u : FinNat n) (h : u.1.+1 < n.+1) : succ_finnat u = (u.1.+1; h).
proof: Proof. by apply path_sigma_hprop. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin