feat(RingTheory/PowerSeries/Inverse): add two lemmas on the normalization of `(X : PowerSeries k)`

[faenuccio]

Add two lemmas about the element X as term of the normalization monoid $k[[X]]$ for a field k.

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