Commit 2021-10-06 10:12 8c657818

refactor(data/nat/basic): remove sub lemmas (#9544)

• Remove the nat sub lemmas that are special cases of lemmas in algebra/order/sub
• This PR does 90% of the work, some lemmas require a bit more work (which will be done in a future PR)
• Protect ordinal.add_sub_cancel_of_le
• Most fixes in other files were abuses of the definitional equality of n < m and nat.succ n \le m.
• This gives the list of renamings.
• The regex to find 90+% of the occurrences of removed lemmas. Some lemmas were not protected, so might not be found this way.

nat.(le_sub_add|add_sub_cancel'|sub_add_sub_cancel|sub_cancel|sub_sub_sub_cancel_right|sub_add_eq_add_sub|sub_sub_assoc|lt_of_sub_pos|lt_of_sub_lt_sub_right|lt_of_sub_lt_sub_left|sub_lt_self|le_sub_right_of_add_le|le_sub_left_of_add_le|lt_sub_right_of_add_lt|lt_sub_left_of_add_lt|add_lt_of_lt_sub_right|add_lt_of_lt_sub_left|le_add_of_sub_le_right|le_add_of_sub_le_left|lt_add_of_sub_lt_right|lt_add_of_sub_lt_left|sub_le_left_of_le_add|sub_le_right_of_le_add|sub_lt_left_iff_lt_add|le_sub_left_iff_add_le|le_sub_right_iff_add_le|lt_sub_left_iff_add_lt|lt_sub_right_iff_add_lt|sub_lt_right_iff_lt_add|sub_le_sub_left_iff|sub_lt_sub_right_iff|sub_lt_sub_left_iff|sub_le_iff|sub_lt_iff)[^_]