fix(Dusart): make corollary_5_3_a a strict inequality

[Chessing234]

Motivation

Dusart / Art01 use a strict lower bound for π(x) at x ≥ 5393. corollary_5_3_a was stubbed with non-strict ≥, which disagreed with TMEEMT.pi_inequality and the cited paper.

Scope

Rebased onto current main. The π* / Buthe ψ index-from-1 fixes from the earlier tip are already on main, so this PR keeps only:

• Dusart.corollary_5_3_a: docstring + statement use >
• TMEEMT.pi_inequality comment aligned with the now-strict corollary

Test plan

• CI Lean build

[Chessing234]

awaiting-review

[Chessing234]

Superseded by #1713 (combine; drops Dusart 5.3(a) strictness).

[Chessing234]

reopening — the indexing fixes landed, but the strict 5.3(a) statement remains needed; branch needs rebase.

[Chessing234]

reopening for the dusart 5.3(a) strictness that #1713 dropped; will rebase onto tip next.

[teorth]

Cross-PR coordination note: this PR tightens Dusart.corollary_5_3_a from ≥ to >. Meanwhile #1767 fills TMEEMT.pi_inequality using the current non-strict Dusart.corollary_5_3_a via a midpoint-of-Ico ⌊x⌋₊ (⌊x⌋₊+1) upgrade. The two PRs collide in two ways:

1. Both touch the same comment inside TMEEMT.pi_inequality — text conflict on rebase.
2. If this PR merges first, feat(TMEEMT): fill Dusart1999.pi_inequality from Dusart corollary 5.3(a) #1767's lt_of_lt_of_le hstrict hge type-mismatches because hge is now < rather than ≤.

Suggested resolution: merge this one first (it fixes the API at the right layer of the paper's proof chain). #1767's proof can then collapse to

theorem pi_inequality (x : ℝ) (hx : x ≥ 5393) :
    _root_.pi x > x / (log x - 1) := Dusart.corollary_5_3_a hx

and the midpoint trick becomes unnecessary. Alternatively, @Chessing234 you could consolidate #1708 + #1767 into one PR.