update P24: provide base List function

Src/Problem24.lean

@@ -3,16 +3,25 @@
 (Easy 🌟) Lotto: Draw `N` different random numbers from the set `1..M`.
 -/
 
+/-- List of natural numbers from `1` to `n` -/
+def List.nrange (n : Nat) : List Nat :=
+  match n with
+  | 0 => []
+  | 1 => [1]
+  | n + 1 => nrange n ++ [n + 1]
+
+example : List.nrange 5 = [1, 2, 3, 4, 5] := rfl
+
 -- You can use this function
-#check List.range
+#check List.nrange
 
 def diffSelect (count range : Nat) : IO (List Nat) := do
   -- sorry
   if count > range then
     dbg_trace s!"can't draw {count} different numbers from 1..{range}"
     return []
 
-  let mut univ := List.range (range + 1) |>.drop 1
+  let mut univ := List.nrange range
   let mut result : List Nat := []
   for _ in [0 : count] do
     let (element, rest) ← extractOne univ
@@ -37,6 +46,8 @@ where
 
 #eval diffSelect 1 1
 
+#eval diffSelect 2 2
+
 #eval diffSelect 24 22
 
 #eval diffSelect 6 49