path_nat_fin_zero@{} {n} : fin_to_nat (@fin_zero n) = 0. Proof. simple_induction n n IHn. - reflexivity. - trivial. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.