Commit 2025-06-07 14:10 c9603c6e

chore(Nat): deprecate lemmas which are now in core (#25494) Each of these lemmas has been upstreamed to core, and the deprecations are in favour of exactly identical statements. Renames:

• Nat.mul_right_eq_self_iff -> Nat.mul_eq_left
• Nat.mul_left_eq_self_iff -> Nat.mul_eq_right
• Nat.eq_zero_of_double_le -> Nat.eq_zero_of_two_mul_le
• Nat.eq_zero_of_le_half -> Nat.eq_zero_of_le_div_two
• Nat.le_half_of_half_lt_sub -> Nat.le_div_two_of_div_two_lt_sub
• Nat.half_le_of_sub_le_half -> Nat.div_two_le_of_sub_le_div_two
• Nat.div_le_of_le_mul' -> Nat.div_le_of_le_mul
• Nat.div_le_self' -> Nat.div_le_self Best reviewed commit-by-commit.