feat(RingTheory/PowerSeries/Order): add properties of the $X$-adic valuation on `PowerSeries X`

[faenuccio]

Add several properties of the $X$-adic valuation on the ring $K[[X]]$ when $K$ is a field. It depends on #13065.

Co-authored-by: María Inés de Frutos-Fernández @mariainesdff