Commit 2022-11-09 03:23 6b921b20

chore(data/nat/basic): drop some nat-specific lemmas (#17400)

• Drop nat.mul_left_inj, nat.mul_right_inj, nat.mul_left_injective, and nat.mul_right_injective. Use general cancel_monoid_with_zero lemmas instead.
• Fix proofs broken by this API change.
• Assume ≠ 0 instead of 0 < in nat.div_div_self.