feat: cleanup some Nat lemmas

[fgdorais]

Depends on #182

Potentially breaking changes:

• Changed Nat.mul_lt_mul (1 use in Mathlib). See comments below.
• Made two parameters implicit in Nat.lt_add_right (4 uses in Mathlib)
• Made parameters implicit for Nat.add_le_add_iff_left (no uses in Mathlib)
• Made parameters implicit for Nat.add_le_add_iff_right (no uses in Mathlib)
• Made parameters implicit for Nat.add_lt_add_iff_left (no uses in Mathlib)
• Made parameters implicit for Nat.add_lt_add_iff_right (no uses in Mathlib)
• Made parameters implicit for Nat.dvd_iff_mod_eq_zero (16 uses in Mathlib)
• Renamed Nat.max_le (no uses in Mathlib) to Nat.max_le_iff and added new Nat.max_le (Mathlib conformance)
• Renamed Nat.le_min (no uses in Mathlib) to Nat.le_min_iff and added new Nat.le_min (Mathlib conformance)
• Protected Nat.zero_le (unknown uses in Mathlib; at least one hiding clause)
• Protected Nat.one_pos (unknown uses in Mathlib)
• Protected Nat.two_pos (no uses in Mathlib)
• Deprecated Nat.lt_min (no uses in Mathlib)
• Deprecated Nat.add_le_to_le_sub (no uses in Mathlib)
• Deprecated Nat.succ_add_eq_succ_add (4 uses in Mathlib)
• Deprecated Nat.mul_le_mul_of_nonneg_left (4 uses in Mathlib)
• Deprecated Nat.mul_le_mul_of_nonneg_right (3 uses in Mathlib)
• Deprecated Nat.mul_lt_mul' (2 uses in Mathlib)
• Deprecated Nat.zero_max (1 use in Mathlib)
• Deprecated Nat.zero_min (no uses in Mathlib)
• Deprecated Nat.max_zero (no uses in Mathlib)
• Deprecated Nat.min_zero (no uses in Mathlib)

Deprecated lemmas all have recommended replacements.

[fgdorais]

Regarding #118: I'm tempted to rename Nat.mul_lt_mul₀ to just Nat.mul_lt_mul. There are some issues:

• On the one hand, Mathlib has mul_lt_mul₀ in Mathlib.Algebra.Order.WithZero so it makes sense to use the same name. On the other hand, like every theorem in that file, the subscript zero indicates WithZero which doesn't make much sense as a distinction in Nat.
• On the one hand, there is a deprecated Nat.mul_lt_mul with one use in Mathlib. On the other hand, the old Nat.mul_lt_mul was a bad theorem with unnecessarily strong hypotheses, so it's a good riddance.

[fgdorais]

I finally opted for Nat.mul_lt_mul over Nat.mul_lt_mul₀. What tipped the scale for me is that the old Nat.mul_lt_mul was just a bad theorem. Existing uses can be replaced by Nat.mul_lt_mul_of_lt_of_le after adapting the hypotheses.

[fgdorais]

Now broken up into smaller pieces.