Commit 2021-10-08 10:04 6c9eee4b

refactor(data/finsupp/basic): remove sub lemmas (#9603)

• Remove the finsupp sub lemmas that are special cases of lemmas in algebra/order/sub, namely:
  • finsupp.nat_zero_sub
  • finsupp.nat_sub_self
  • finsupp.nat_add_sub_of_le
  • finsupp.nat_sub_add_cancel
  • finsupp.nat_add_sub_cancel
  • finsupp.nat_add_sub_cancel_left
  • finsupp.nat_add_sub_assoc
• Rename the remaining lemmas to use tsub:
  • finsupp.coe_nat_sub → finsupp.coe_tsub
  • finsupp.nat_sub_apply → finsupp.tsub_apply Lemmas in algebra/order/sub will soon also use tsub (see Zulip)