chore(combinatorics/quiver/path): reduce imports (#17216)
By using some lower-tech theorems, we can avoid importing the entire `algebra.order` hierarchy, significantly reducing the import dependencies of the basic category theory library.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
