Commit 2021-10-25 17:42 312db88b

feat(*): use ordered_sub instead of nat.sub lemmas (#9855)

• For all nat.sub lemmas in core, prefer to use the has_ordered_sub version.
• Most lemmas have an identical version for has_ordered_sub. In some cases we only have the symmetric version.
• Make arguments to tsub_add_eq_tsub_tsub and tsub_add_eq_tsub_tsub_swap explicit
• Rename add_tsub_add_right_eq_tsub -> add_tsub_add_eq_tsub_right (for consistency with the _left version)
• Rename sub_mul' -> tsub_mul and mul_sub' -> mul_tsub (these were forgotten in #9793)
• Many of the fixes are to fix the identification of n < m and n.succ \le m.
• Add projection notation h.nat_succ_le for nat.succ_le_of_lt h.