fix: remove use of native_decide in the HTTP library

[algebraic-dev]

This PR removes the use of native_decide in the HTTP library and adds proofs to remove the panic!.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 71ff36621103dfab119dfbead39dea3995d5832d --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-10 01:07:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 71ff36621103dfab119dfbead39dea3995d5832d --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-10 13:53:19)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 71ff36621103dfab119dfbead39dea3995d5832d --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-10 01:07:09)

[TwoFX]

Looks good, just some minor nitpicks.