Update LehmerCode.agda

made it export `factorial` so nothing else in the library that depends on `factorial` being exported breaks

Author: anshwad10

Cubical/Data/Fin/LehmerCode.agda

@@ -22,6 +22,7 @@ open import Cubical.Relation.Nullary
 open import Cubical.Data.Unit as ⊤
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Properties using (factorial) public
 open import Cubical.Data.Nat.Order
 open import Cubical.Data.Fin.Base as F
 open import Cubical.Data.Fin.Properties