Optimizations to `nat_valuation_aux`

[Vierkantor]

This breaks some proofs but it seems to provide a 20%-30% speedup on the tests (and doesn't fail the tests!)

[alexjbest]

Thanks!