Add quicksort implementations with formal proof and Rust reference#1

honicky wants to merge 2 commits into

claude/formalize-mercers-theorem-7R430honicky/fun-with-lean:claude/formalize-mercers-theorem-7R430from

claude/quicksort-rust-lean-proof-qjJCwhonicky/fun-with-lean:claude/quicksort-rust-lean-proof-qjJCwCopy head branch name to clipboard