finnat_ind@{u} (P : forall n : nat, FinNat n -> Type@{u}) (z : forall n : nat, P n.+1 (zero_finnat n)) (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u)) {n : nat} (u : FinNat n) : P n u. Proof. simple_induction n n IHn; intro u. - elim (not_lt_zero_r u.1 u.2). - destruct u as [x h]. destruct x as [| x]. + nrefine (transport (P n.+1) _ (z _)). by apply path_sigma_hprop. + refine (transport (P n.+1) (path_succ_finnat _ _) _). apply s. apply IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoids Require Import Types.Empty Types.Sigma Types.Sum Types.Prod Types.Equiv. Require Import Spaces.Nat.Core. Require Import Finite.Fin.