cleanup in FinNat

theories/Spaces/Finite/FinNat.v

@@ -10,36 +10,18 @@
 
 Definition FinNat (n : nat) : Type0 := {x : nat | x < n}.
 
-Definition path_finnat {n : nat} (x : nat) (h1 h2 : x < n)
-  : (x; h1) = (x; h2) :> FinNat n.
-Proof.
-  by apply path_sigma_hprop.
-Defined.
-
 Definition zero_finnat (n : nat) : FinNat n.+1
   := (0; _ : 0 < n.+1).
 
 Definition succ_finnat {n : nat} (u : FinNat n) : FinNat n.+1
   := (u.1.+1; leq_succ u.2).
 
-Lemma path_succ_finnat {n : nat} (x : nat) (h : x.+1 < n.+1)
-  : succ_finnat (x; leq_pred' h) = (x.+1; h).
-Proof.
-  by apply path_finnat.
-Defined.
-
 Definition last_finnat (n : nat) : FinNat n.+1
   := exist (fun x => x < n.+1) n (leq_refl n.+1).
 
 Definition incl_finnat {n : nat} (u : FinNat n) : FinNat n.+1
   := (u.1; leq_trans u.2 (leq_succ_r (leq_refl n))).
 
-Lemma path_incl_finnat (n : nat) (u : FinNat n) (h : u.1 < n.+1)
-  : incl_finnat u = (u.1; h).
-Proof.
-  by apply path_sigma_hprop.
-Defined.
-
 Definition finnat_ind@{u} (P : forall n : nat, FinNat n -> Type@{u})
   (z : forall n : nat, P n.+1 (zero_finnat n))
   (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
@@ -50,9 +32,10 @@
   - elim (not_lt_zero_r u.1 u.2).
   - destruct u as [x h].
     destruct x as [| x].
-    + exact (transport (P n.+1) (path_finnat _ _ h) (z _)).
-    + refine (transport (P n.+1) (path_succ_finnat x h) _).
-      apply s. apply IHn.
+    + nrefine (transport (P n.+1) _ (z _)).
+      by apply path_sigma_hprop.
+    + refine (transport (P n.+1) _ (s _ _ (IHn (x; leq_pred' _)))).
+      by apply path_sigma_hprop.
 Defined.
 
 Lemma compute_finnat_ind_zero@{u} (P : forall n : nat, FinNat n -> Type@{u})
@@ -63,7 +46,7 @@
 Proof.
   snrapply (transport2 _ (q:=1)).
   rapply path_ishprop.
 Defined.
 
 Lemma compute_finnat_ind_succ@{u} (P : forall n : nat, FinNat n -> Type@{u})
   (z : forall n : nat, P n.+1 (zero_finnat n))
@@ -72,7 +55,7 @@
   {n : nat} (u : FinNat n)
   : finnat_ind P z s (succ_finnat u) = s n u (finnat_ind P z s u).
 Proof.
-  destruct u as [u1 u2]; simpl; unfold path_succ_finnat.
+  destruct u as [u1 u2]; simpl.
   destruct (path_ishprop u2 (leq_pred' (leq_succ u2))).
   refine (transport2 _ (q:=1) _ _).
   rapply path_ishprop.
@@ -113,30 +96,12 @@
   apply path_nat_fin_zero.
 Defined.
 
-Lemma path_fin_to_finnat_fin_incl {n : nat} (k : Fin n)
-  : fin_to_finnat (fin_incl k) = incl_finnat (fin_to_finnat k).
-Proof.
-  reflexivity.
-Defined.
-
-Lemma path_fin_to_finnat_fin_last (n : nat)
-  : fin_to_finnat (@fin_last n) = last_finnat n.
-Proof.
-  reflexivity.
-Defined.
-
 Lemma path_finnat_to_fin_succ {n : nat} (u : FinNat n)
   : finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u).
 Proof.
   cbn. do 2 f_ap. by apply path_sigma_hprop.
 Defined.
 
-Lemma path_finnat_to_fin_zero (n : nat)
-  : finnat_to_fin (zero_finnat n) = fin_zero.
-Proof.
-  reflexivity.
-Defined.
-
 Lemma path_finnat_to_fin_incl {n : nat} (u : FinNat n)
   : finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u).
 Proof.