is_bounded_fin_to_nat@{} {n} (k : Fin n) : fin_to_nat k < n. Proof. induction n as [| n IHn]. - elim k. - destruct k as [k | []]; exact _. 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.