Theorem cmpUsing_eq_gt

Modification history

2024-02-20 12:29

Mathlib/Init/Data/Ordering/Lemmas.lean

chore: Remove `Init.IteSimp` (#10708) …

Modified cmpUsing_eq_gt View on Github →

2023-05-24 01:45

Mathlib/Init/Data/Ordering/Lemmas.lean

feat: port Init.Data.Ordering.Lemmas (#4281)

Added cmpUsing_eq_gt View on Github →