refactor(data/nat/log): Golf + improved theorem names (#14019)
Other than golfing and moving a few things around, our main changes are:
- rename `log_le_log_of_le` to `log_mono_right`, analogous renames elsewhere.
- add `lt_pow_iff_log_lt` and a `clog` analog.
