feat: add Triple.post_imp_elim and Triple.rotate_pre

[sgraf812]

This PR adds two Hoare triple lemmas to Std.Do. Triple.post_imp_elim eliminates an implication in the postcondition: a specification ⦃P⦄ x ⦃Q⦄ upgrades a proof of ⦃P⦄ x ⦃Q →ₚ R⦄ to ⦃P⦄ x ⦃R⦄. Triple.rotate_pre proves a triple for prog from a specification of an observation p by rotating p into program position with the goal wp⟦prog⟧ Post as its postcondition, so that mvcgen can step through p.

This supports specifications written in the object language, where a programmatic precondition such as (pre x).holds appears as a triple hypothesis. The premise hp of rotate_pre states that successful runs of p leave the state unchanged; it holds for every program of a stateless monad such as Except. 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)

[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)