n k : (nat_fin n k + nat_fin_compl n k).+1 = n. Proof. simple_induction n n IHn; intro k. - contradiction. - destruct k as [k|?]; simpl. + rewrite nat_add_comm. specialize (IHn k). rewrite nat_add_comm in IHn. exact (ap S IHn). + rewrite nat_add_comm; reflexivity. Qed.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.