feat(tactic/positivity): Extension for `coe` (#16141)
Add:
* a case in the main `positivity` tactic to show that `0 ≤ a` in a `canonically_ordered_add_monoid`
* `positivity_coe`, an extension to `positivity`, to turn `0 ≤ a`/`0 < a` into `0 ≤ ↑a`/`0 < ↑a` when `a` is of type `ℕ`, `ℤ`, `ℚ`.
