perf: optimize the expensive portions of DivRem proofs

[dtumad]

Each of the soundness proofs for DivRem share a large tail with essentially the same proof obligation, and circuit_proof_start is especially slow with DivRem. This PR introduces adds a lemma that reduces the soundness proof obligation to just the instruction soundness (handling the readers and is_real etc.), and introduces a custom DivRem.spec_proof_start tactic that does slightly less unfolding than circuit_proof_start.

Performance

The nine DivRem soundness conjuncts (Div/Divu/Divuw/Divw/Rem/Remu/Remuw/Remw + Reader) each proved a full GeneralFormalCircuit.Soundness over the same main, re-elaborating a byte-identical ~265-line Operations.Requirements tail at 128M heartbeats — i.e. the same readers/is_real/channel work done nine times. This PR extracts that tail into Soundness/Tail.lean:

• requirements_holds proves the shared tail once, on raw (un-circuit_proof_start'd) binders;
• SpecObligation / soundness_of_specObligation reassemble a full Soundness from a per-conjunct spec plus that shared tail;
• the new spec_proof_start elab tactic mirrors circuit_proof_start's setup but unfolds SpecObligation, so each conjunct does less work and proves only its chip-specific Spec.

Net effect (fresh isolated compile-time profile on this branch — docs/snapshots/compile-profile.md): the shared tail now costs 123.6s once instead of inline in every conjunct, and each conjunct's body is the chip-specific spec proof (8 div/rem conjuncts at 277–307s, Reader 68s) rather than spec + tail. The diff removes ~270 lines from each of the nine files (+552 / −2512 overall). requirements_holds is axiom-clean ([propext, Classical.choice, Quot.sound]), and lake build SP1Clean stays green (3676 jobs).

See docs/snapshots/compile-profile.md for the full per-module profile.

[dtumad]

Handled by #104