fsucc_mod@{} {n : nat} : Fin n -> Fin n. Proof. destruct n. 1: exact idmap. intros [x|]. - exact (fsucc x). - exact fin_zero. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.