mathlib

c2777528 - feat(algebra/group/defs, data/nat/basic): some `ne` lemmas (#6637)

feat(algebra/group/defs, data/nat/basic): some `ne` lemmas (#6637) `≠` versions of `mul_left_inj`, `mul_right_inj`, and `succ_inj`, as well as the lemma `succ_succ_ne_one`.