Commit 2026-02-06 22:51 23f9fd8a

View on Github →

chore(Order/Cover): use to_dual (#34880) We add a lot of to_dual none tags, as a lot of the generated lemmas just swap the order of equalities, or other arguments inside quantifiers.

Estimated changes

deleted theorem CovBy.ge_of_gt
deleted theorem CovBy.ne'
deleted theorem CovBy.unique_right
deleted theorem WCovBy.ge_of_gt
deleted theorem WCovBy.inf_eq
deleted theorem covBy_iff_le_iff_lt_right
deleted theorem covBy_iff_lt_iff_le_right