padic_norm file maintenance

[BoltonBailey]

There are still probably things that can be done to improve the number_theory/padic_norm.lean. Some ideas:

• Split the file in two at the definition padic_norm with that latter part being called padic_norm.lean and the first part being padic_val.lean. See [Merged by Bors] - refactor(number_theory/padics/padic_norm): split file #13576
• There are a lot of lemmas with [prime p] typeclass argument which are actually only need something like p \ne 1. Perhaps some of these are useful, but they could be named more consistently.
• Perhaps we could do a better job of ordering lemmas, I think there are several padic_val_nat sections.
• As I think Michael Stoll suggested, it may be better to put the definition of padic_val_int before padic_val_nat.

Originally posted by @BoltonBailey in #12454 (comment)