Commit 2026-01-12 12:26 21cf59b0
View on Github →feat: prove Prod.wellFoundedLT directly (#33771)
Prove Prod.wellFoundedLT without going through Antisymmetrization. This makes the instance accessible without having to import antisymmetrization. Remove Prod.wellFoundedLT' since it's not useful anymore. Use @[to_dual] for Prod.wellFoundedLT.