Lean: stop 'exponent exceeds threshold' warnings with huge literal powers

When a statement mentions something like 4444 ^ 4444, exact Nat.pow_lt_pow_left h1 h2 and rw [pow_mul] on it raise 'exponent 4444 exceeds the threshold 256, exponentiation operation was not evaluated'. The cause is the unifier trying to reduce the literal power. Fix: prove the fact for a variable exponent, have key : ∀ n ≠ 0, 4444 ^ n < (10 ^ 4) ^ n := fun n hn => Nat.pow_lt_pow_left (by norm_num) hn, then instantiate with key 4444 (by norm_num). Next, generalize 4444 ^ 4444 = N at h1 h2 ⊢ so omega and friends see an atom. Also: List.sum_le_card_nsmul is deprecated. Use List.sum_le_length_nsmul (import Mathlib.Algebra.Order.BigOperators.Group.List), then simp only [nsmul_eq_mul, Nat.cast_id].