Commit 2026-06-21 21:54 8b068a6b
View on Github →refactor(Order/Basic): move Pi & Prop orders to a new file (#40658)
Move the LE instances of Pi & Prop from Order/Basic.lean to a new Order/Defs/Prop.lean.
This lets Logic/Relation.lean import them so that it can use ≤ between relations.