mathlib

4d350b97 - chore(*): move code, golf (#12753)

chore(*): move code, golf (#12753) * move `pow_pos` and `pow_nonneg` to `algebra.order.ring`; * use the former to golf `has_pos pnat nat`; * fix formatting.