feat(Algorithms/Lean): add timed insertion sort

[ps600779]

feat(Algorithms/Lean): add timed insertion sort

Summary

• add a new Cslib.Algorithms.Lean.InsertionSort.InsertionSort module defining timed orderedInsert and insertionSort
• prove that the timed algorithms agree with Mathlib’s list insertion sort, and establish sortedness and permutation correctness
• bound the comparison cost of insertionSort by n * n and export the new module from Cslib.lean

Validation

• lake exe mk_all --module
• lake build
• lake test
• lake exe checkInitImports
• lake exe lint-style Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
  If you want a slightly more specific title, this also fits CSLib’s convention:
  feat(Algorithms/Lean): add verified timed insertion sort

[Copilot]

Pull request overview

Adds a new timed (comparison-counting) insertion sort development to CSLib’s Lean algorithms area, including correctness theorems relating it to Mathlib’s insertion sort and a simple quadratic upper bound on comparison cost.

Changes:

• Introduces orderedInsert and insertionSort as TimeM ℕ (List α) computations, with comparisons counted via ✓.
• Proves functional agreement with Mathlib’s List.orderedInsert / List.insertionSort, and derives sortedness + permutation correctness.
• Establishes a recurrence-based time bound and exports the new module from Cslib.lean.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean	New timed insertion sort implementation with correctness + time-bound proofs.
Cslib.lean	Exports the new insertion sort module from the root import file.

[Shreyas4991]

Duplicate of several prior PRs on insertion sort.