fix(proofs): add allTake/fromLteTrue lemmas + extend path_claims tests

[hyperpolymath]

SafetyLemmas.idr:

• allTake: allRec p xs = True → allRec p (take n xs) = True
• fromLteTrue: (a <= b) = True → LTE a b
• falseImpliesNotTrue: refactored to work for any Bool b, not just False

mcp-bridge/tests/path_claims_test.js: additional claim coverage

Summary

Changes

RSR Quality Checklist

Required

• Tests pass (just test or equivalent)
• Code is formatted (just fmt or equivalent)
• Linter is clean (no new warnings or errors)
• No banned language patterns (no TypeScript, no npm/bun, no Go/Python)
• No unsafe blocks without // SAFETY: comments
• No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry)
• SPDX license headers present on all new/modified source files
• No secrets, credentials, or .env files included

As Applicable

• .machine_readable/STATE.a2ml updated (if project state changed)
• .machine_readable/ECOSYSTEM.a2ml updated (if integrations changed)
• .machine_readable/META.a2ml updated (if architectural decisions changed)
• Documentation updated for user-facing changes
• TOPOLOGY.md updated (if architecture changed)
• CHANGELOG or release notes updated
• New dependencies reviewed for license compatibility (MPL-2.0 / MPL-2.0)
• ABI/FFI changes validated (src/abi/ and ffi/zig/ consistent)

Testing

Screenshots

[hyperpolymath]

Closing as superseded by current main: the path_claims test reset changes and falseImpliesNotTrue/fromLteTrue updates have landed, and main already carries allTake in the core allRec lemma section after #237 removed the duplicate.