Reframe z3py guide intro around Lean as symbolic reasoning engine

[kiranandcode]

Summary

• Rewrites the z3py guide intro to lead with Lean 4 as a general-purpose symbolic reasoning engine, rather than framing it as "theorem provers are hard, we make them easy"
• Drops slop: "eliminates it", "bread and butter", "pays off most visibly", dramatic two-sentence antithesis in the limitations section
• Keeps all code examples and technical sections intact

Test plan

• make -C docs html builds cleanly