Commit 2021-08-02 11:38 25a42309

chore(data/real/basic): cleanup (#8501)

• use is_lub etc in the statement of real.exists_sup, rename it to real.exists_is_lub;
• move parts of the proof of real.exists_is_lub around;