Remove duplicated factorial function (agda#1183)

`_!` is defined in `Cubical.Data.Nat.Properties`, `factorial` is defined in `Cubical.Data.Fin.LehmerCode`, and they both have identical definitions.

Author: anshwad10

Cubical/Data/Fin/LehmerCode.agda

@@ -191,11 +191,11 @@ encode = equivFun lehmerEquiv
 decode : LehmerCode n → Fin n ≃ Fin n
 decode = invEq lehmerEquiv
 
+-- Use the one in Cubical.Data.Nat.Properties instead
 factorial : ℕ → ℕ
-factorial zero = 1
-factorial (suc n) = suc n · factorial n
+factorial = _!
 
-lehmerFinEquiv : LehmerCode n ≃ Fin (factorial n)
+lehmerFinEquiv : LehmerCode n ≃ Fin (n !)
 lehmerFinEquiv {zero} = isContr→Equiv isContrLehmerZero isContrFin1
 lehmerFinEquiv {suc n} = _ ≃⟨ invEquiv lehmerSucEquiv ⟩
                          _ ≃⟨ ≃-× (idEquiv _) lehmerFinEquiv ⟩