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). 





leanprover-community/mathlib,leanprover-community/mathlib