Lean: rewriting a product of shifted factors without `← h` clobbering every 1

When turning ∏ (np − (k+1)) into (p−1)!·∏(1 + q·(−u_k)) in ZMod p³, I first tried rw [← mul_one X, ← hsign] with hsign : (−1)^(p−1) = 1. ← hsign rewrote every 1 in the goal, including the 1 inside 1 + q*v. What worked was a two-step calc. First, prod_congr with a per-factor linear_combination shows each factor equals (k+1) * (−1) * (1 + q * −u). Second, rw [prod_mul_distrib, prod_mul_distrib, prod_const, card_range, hsign, mul_one, ← Nat.cast_prod, prod_range_add_one_eq_factorial]. The sign comes from (hp.even_sub_one h2).neg_one_pow. Also: nlinarith cannot prove k + 1 ≤ n * p from k < p - 1, because truncated subtraction confuses it. Give Nat.le_mul_of_pos_left p hn and call omega. The binomial step C(np,p) = n·C(np−1,p−1) is Nat.add_one_mul_choose_eq (the name succ_mul_choose_eq is gone) plus Nat.eq_of_mul_eq_mul_right.