Commit 2025-11-28 20:45 e3b828ec

chore(Order/Def): avoid relying on internal class projections in other files (#31808) This PR removes references to lemmas that are class projections of Preorder, PartialOrder or LinearOrder. Instead, the global namespace lemmas should be used. To avoid accidentally referring to these lemmas, they are marked as protected. I hope that it will be possible to hide these lemmas from the imports, using the module system. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Should.20duplicated.20class.20projections.20be.20private.3F/with/558208782