Factorial cancellation for the actual binomially grouped forcing terms.

theorem AVenhance.Infra.Section4.iterate_choose_factorial_shift_le (n j a : ℕ) (hj : j ≤ n) : n.choose j * j.factorial * (n - j + a).factorial ≤ (n + a).factorial

Shifted analytic scalar weights absorb the exact coefficient multiplicity.