mathlib3

ce0498e6 - feat(data/nat/basic): add injectivity and divisibility lemmas (#5068)

feat(data/nat/basic): add injectivity and divisibility lemmas (#5068) Multiplication by a non-zero natural is injective. Also a simple criterion for non-divisibility which I couldn't find (0<b<a implies a doesn't divide b).