chore(*): golf using new `positivity` tactic (#15701)
The `positivity` tactic introduced in #15618 solves goals of the form `0 < x` and `0 ≤ x`, particularly motivated by streamlining bigger inequality calculations where these frequently show up as side goals. This PR gives a few example uses in this kind of bigger inequality calculation, golfing proofs in:
- archive/imo/imo2005_q3
- archive/imo/imo2013_q5
- analysis/convex/basic
- analysis/mean_inequalities_pow
- topology/algebra/order/basic
