Commit 2026-03-20 23:33 e42eb8d4

feat(Order/Interval/Set/Disjoint): use to_dual (#36822) This PR tags some theorems about Disjoint with to_dual. Unlike #33140, Disjoint is not translated to Codisjoint, because it is used on Set or Filter. This puts us in the awkward position that the name translation mistakenly thinks the new declaration name should have disjoint replaced with codisjoint. So I have to add the names manually. I don't see an easy fix for this. Also removed simp from Ioi_disjoint_Iio_same, because Iio_disjoint_Ioi_iff subsumes it.