Auxiliary order lemmas for the Aharoni-Korman import

This module collects helper lemmas used by the Aharoni-Korman counterexample.