feat(Data/Finset/Range): add strictMono_range (leanprover-community#39557)

Author: b-mehta

Mathlib/Data/Finset/Range.lean

@@ -92,6 +92,9 @@ theorem range_subset_range {n m} : range n ⊆ range m ↔ n ≤ m := by grind
 
 theorem range_mono : Monotone range := fun _ _ => range_subset_range.2
 
+theorem strictMono_range : StrictMono range :=
+  strictMono_nat_of_lt_succ fun _ ↦ by simp [ssubset_def]
+
 theorem mem_range_succ_iff {a b : ℕ} : a ∈ range b.succ ↔ a ≤ b := by grind
 
 theorem mem_range_le {n x : ℕ} (hx : x ∈ range n) : x ≤ n := by grind