mathlib3
7a7fadaf - refactor(data/nat/basic): finish removing sub lemmas (#9601)

Commit
4 years ago
refactor(data/nat/basic): finish removing sub lemmas (#9601) * Follow-up of #9544 to remove the remaining sub lemmas on `nat` that can be generalized to `has_ordered_sub`. * The renamings of the lemmas in mathlib that occurred at least once: ``` nat.sub_eq_of_eq_add -> sub_eq_of_eq_add_rev nat.add_sub_sub_cancel -> add_sub_sub_cancel' nat.sub_le_self -> sub_le_self' ```
Author
Parents
Loading