feat(order/cover): congr lemmas for `covby` (#15663)
We prove that `antisymm_rel (≤) a b` and `a ⋖ c` implies `b ⋖ c`, and variations thereof.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
