#1790 (Oct 12, 2022, 12:50:08 AM)

1. merged (detail / hgweb)
2. adjusted proofs (detail / hgweb)
3. added and reorganized lemmas (some suggested by Jeremy Sylvestre) (detail / hgweb)
4. removed redundant lemma (detail / hgweb)
5. moved theorem from Fun to Set (detail / hgweb)
6. added lemmas antisymp_ge[simp], antisymp_greater[simp], antisymp_le[simp], and antisymp_less[simp] (detail / hgweb)
7. added lemmas reflp_ge[simp] and reflp_le[simp] (detail / hgweb)

Started by an SCM change

This run spent:

• 7.1 sec waiting;
• 1 hr 51 min build duration;
• 1 hr 51 min total from scheduled to completion.