Fix LCNF extraction bugs: Bool-param branch inversion & binary min/max operand drop

[emeryberger]

Fix two LCNF extraction bugs found extracting real-world code

While using LeanToPython to extract verified algorithms from
Scalene's profiler into Python, two
extraction bugs surfaced. Both are fixed here with regression coverage; the
existing correctness suite stays at LCNF 132/132 (and the two
previously-failing mod_pow/fast_pow Bool cases now pass).

1. Bool-typed-parameter branch inversion (silent wrong answer)

if boolParam then a else b lowers to a Decidable cases on
instDecidableEqBool boolParam true. emitDecidableCases chose branch order
from a name heuristic (_x/x/b/cond/…). A Bool parameter whose name
wasn't on that list (e.g. isMalloc, flag) fell through to the
"Nat matched against 0" path, which swaps the branches — emitting

def fpd(is_malloc, count):
    if is_malloc:
        return -count      # WRONG — this is the `else` body
    else:
        return count

for if isMalloc then count else -count.

Fix: track each fvar's LCNF Bool type (boolTypedVars, populated for
params in emitFunParams and lets in emitLetValue) and resolve the
discriminant through the alias map (the Decidable node aliases to the
underlying Bool fvar). Bool-typed discriminant → normal branch order;
otherwise fall back to the existing name heuristic.

2. Binary min/max operand drop

Nat.min/Nat.max map to Python min/max via stdlibFnToPython?, but the
"simple wrapper" emitter passed only the last argument, so Nat.min a b
became min(b) — dropping the first operand (and crashing on assoc-list
inputs). Fix: for min/max, emit all value operands.

Tests

RegressionFixes.lean + RegressionFixes_test.py extract and execute both
patterns and assert correct results:

lake env lean RegressionFixes.lean > RegressionFixes_out.py
python3 RegressionFixes_test.py   # OK: Bool-branch order, binary min/max