feat(order/zorn): Added some results about chains (#10658)
Added `chain_empty`, `chain_subsingleton`, and `chain.max_chain_of_chain`.
The first two of these are immediate yet useful lemmas. The last one is a consequence of Zorn's lemma, which generalizes Hausdorff's maximality principle.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
