feat: add Triple.observe

[sgraf812]

This PR adds the Hoare triple lemma Triple.observe to Std.Do. It proves a triple for prog from a specification of a stateless program obs: observing the postcondition Q of obs (via h) and using Q to establish wp⟦prog⟧ Post (via hgoal) yields ⦃Pre⦄ prog ⦃Post⦄. The premise hp requires obs to be stateless: its successful runs leave the state unchanged, which holds for every program of a stateless monad such as Except.

This supports specifications written in the object language, where a programmatic precondition such as (pre x).holds appears as a triple hypothesis, which mvcgen then steps through. Tests exercise the pattern for unfoldable and opaque Except programs.

[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 aa2317ae0bf993eabeefe5aad010a90a83e54287 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-12 19:51:40)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase aa2317ae0bf993eabeefe5aad010a90a83e54287 --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-17 09:49:17)

[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 aa2317ae0bf993eabeefe5aad010a90a83e54287 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-12 19:51:42)