Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-29 13:12 fe29f883

View on Github →

feat(data/nat/basic): (n+1) / 2 ≤ n (#6863) Zulip: https://leanprover.zulipchat.com/#narrow/stream/116395-maths

Estimated changes

added theorem nat.div_eq_sub_mod_div
added theorem nat.lt_iff_le_pred
added theorem nat.lt_mul_div_succ
added theorem nat.mod_div_self
added theorem nat.mul_div_le