Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-09 17:02 a2810d97

View on Github →

feat(data/int/basic): coercion subtraction inequality (#10054) Adding to simp a subtraction inequality over coercion from int to nat

Estimated changes