Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-22 04:37 1741a1d6

View on Github →

feat(data/nat/basic): division inequalities (#1579)

feat(data/nat/basic): division inequalities
whitespace
fix
shorten proof

Estimated changes

Modified src/data/nat/basic.lean

added theorem nat.div_mul_div_le_div

added theorem nat.mul_div_le_mul_div_assoc