mathlib
38ae9b37 - chore(data/nat/basic): reuse a proof, drop a duplicate (#5836)

Commit
5 years ago
chore(data/nat/basic): reuse a proof, drop a duplicate (#5836) Drop `nat.div_mul_le_self'`, use `nat.div_mul_le_self` instead.
Author
Parents
Loading