Commit 2022-05-31 09:48 615babaf

feat(order/monotone): prove nat.exists_strict_mono etc (#14435)

• add nat.exists_strict_mono, nat.exists_strict_anti, int.exists_strict_mono, and int.exists_strict_anti;
• move set.Iic.no_min_order and set.Ici.no_max_order to data.set.intervals.basic;
• add set.Iio.no_min_order and set.Ioi.no_max_order;
• add no_max_order.infinite and no_min_order.infinite, use them in the proofs;
• rename set.Ixx.infinite to set.Ixx_infinite;
• add set.Ixx.infinite - lemmas and instances about infinite, not set.infinite.