Commit 2021-10-08 07:33 83a07ce0
View on Github →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_...).