feat(algebra/parity): more general odd.pos (#15186)
The old version of this lemma (added in #13040) was only for ℕ and didn't allow dot notation. We remove this and add a version for `canonically_ordered_comm_semiring`s, and if the definition of `odd` changes, this will also work for `canononically_ordered_add_monoid`s.
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
