Commit 2025-05-29 18:50 1f0a9e77

View on Github →

feat(Order): add gcongr lemmas for Prod.mk (#25301) Add three gcongr lemmas to help decompose explicit elements of a product type. From the ABC-Exceptions project

Estimated changes