mathlib

1158f6d8 - feat(tactic/positivity): Extension for natural powers in a `canonically_ordered_comm_semiring` (#17535)

feat(tactic/positivity): Extension for natural powers in a `canonically_ordered_comm_semiring` (#17535) Provide `positivity_canon_pow`, a positivity extension for `a ^ n` where `a` is in a `canonically_ordered_comm_semiring`. Typically, this applies to `ennreal`, which is not covered by the existing `positivity_pow` extension.