path_nat_fsucc@{} {n : nat} : forall k : Fin n, fin_to_nat (fsucc k) = S (fin_to_nat k). Proof. simple_induction n n IHn. - intros []. - intros [k'|[]]. + rewrite path_fin_fsucc_incl, path_nat_fin_incl. apply IHn. + reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.