mathlib3

83a07ce0 - feat(data/nat/log): add antitonicity lemmas for first argument (#9597)

feat(data/nat/log): add antitonicity lemmas for first argument (#9597) `log` and `clog` are only antitone on bases >1, so we include this as an assumption in `log_le_log_of_left_ge` (resp. `clog_le_...`) and as a domain restriction in `log_left_gt_one_anti` (resp. `clog_left_...`).