[Certora] Do not hide maxLif's denominator in NoDivisionByZero

[MathisGD]

Do not hide maxLif's denominator in this proof

With this summary, NoDivisionByZero.spec no longer executes the two mulDivDown calls inside maxLif, while the rule bodies also never requireInvariant the enabled-LLTV/enabled-cursor bounds they cite. Under CVL rule semantics, the prestate can still have arbitrary storage such as isLltvEnabled[0] and isLiquidationCursorEnabled[WAD] set, so touchMarket would reach maxLif(0, WAD) with a zero denominator in the real code, but this spec proves the call after replacing it with maxLifGhost; either keep maxLif unsummarized for the denominator check or explicitly assume the proven role/market invariants before relying on them.

Useful? React with 👍 / 👎.

Originally posted by @chatgpt-codex-connector[bot] in #992 (comment)

[Yash-arch-ui]

I have reproduced it !!!!! Will you accept an external pr ?