diff --git a/Cubical/Data/Fin/Recursive/Base.agda b/Cubical/Data/Fin/Recursive/Base.agda
index 9dffa719ce..5ba71383d3 100644
--- a/Cubical/Data/Fin/Recursive/Base.agda
+++ b/Cubical/Data/Fin/Recursive/Base.agda
@@ -32,3 +32,7 @@ elim
   → (fn : Fin k) → P fn
 elim {k = suc k} P fz fs zero = fz
 elim {k = suc k} P fz fs (suc x) = fs x (elim P fz fs x)
+
+toℕ : Fin k → ℕ
+toℕ {suc k}   zero  = zero
+toℕ {suc k} (suc n) = suc (toℕ n)
diff --git a/Cubical/Data/Fin/Recursive/Properties.agda b/Cubical/Data/Fin/Recursive/Properties.agda
index ef5dc30d76..455615dbaf 100644
--- a/Cubical/Data/Fin/Recursive/Properties.agda
+++ b/Cubical/Data/Fin/Recursive/Properties.agda
@@ -179,6 +179,10 @@ toFin : (n : ℕ) → Fin (suc n)
 toFin zero = zero
 toFin (suc n) = suc (toFin n)
 
+toFin< : (m : ℕ) → m < n → Fin n
+toFin< {suc n} zero 0<sn = zero
+toFin< {suc n} (suc m) m<n = suc (toFin< m m<n)
+
 inject<#toFin : ∀(i : Fin n) → inject< (≤-refl (suc n)) i # toFin n
 inject<#toFin {suc n} zero = _
 inject<#toFin {suc n} (suc i) = inject<#toFin {n} i