feat(algorithms): add stable insertion sort

[Robertboy18]

This PR adds stable insertion sort! The implementation recursively sorts the tail and then inserts the head into the sorted result. The stability argument is the standard one: because the list is processed from right to left, inserting the current element before equal elements in the already-sorted tail preserves the original order of equal values. Standard insertion sort algorithm from CRLS.

I prove that it satisfies the sortedness, permutation correctness, stability via StableByValue, and a quadratic comparison bound!

Validation:

• lake build Cslib

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds foundational sorting utilities and a timed, stable insertion sort implementation in Lean, including correctness and time-complexity proofs, and re-exports them from the top-level module.

Changes:

• Introduces a StableByValue predicate for expressing stability via per-value filtering.
• Implements TimeM-based insertion sort with comparison-counting, plus correctness/stability/sortedness proofs.
• Exposes the new modules via Cslib.lean imports.

Reviewed changes

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

File	Description
Cslib/Algorithms/Lean/Sorting.lean	Adds StableByValue stability predicate used by sorting proofs.
Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean	Implements timed stable insertion sort with proofs and a time bound.
Cslib.lean	Re-exports the new sorting and insertion sort modules.