Commit 2026-11-02 08:37 abea571d

View on Github →

chore(Order/RelClasses): remove redundant instances (#43608) Some instances can be synthesized but are necessary to help to_dual, so they are kept.

Estimated changes

deleted theorem isTrans_le
deleted theorem isTrans_lt