mathlib
a2810d97 - feat(data/int/basic): coercion subtraction inequality (#10054)

Commit
4 years ago
feat(data/int/basic): coercion subtraction inequality (#10054) Adding to simp a subtraction inequality over coercion from int to nat Co-authored-by: cocohearts <41932135+cocohearts@users.noreply.github.com>
Author
Parents
Loading