Commit 2021-08-02 10:07 69c6adb5
View on Github →chore(data/int): move some lemmas from basic to a new file (#8495)
Move least_of_bdd, exists_least_of_bdd, coe_least_of_bdd_eq,
greatest_of_bdd, exists_greatest_of_bdd, and
coe_greatest_of_bdd_eq from data.int.basic to data.int.least_greatest.