Commit 2020-11-23 01:00 ce0498e6
View on Github →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).