mathlib3

feat(data/nat/basic): division inequalities

#1579

Merged