Extend positive-X-lag auto tactic to non-unit lag coefficients

[PerAlexandersson]

The generalized backend prec_pos_X_lag_combo_sequence already handles
recurrences of the form

P(n+2) = C(a n) * P(n+1) + (C(c n) * X) * P(n)

with a n > 0 and c n >= 0. The explicit tactic frontend also works.

During the generated A128099 transfer,
rr_prec_pos_X_lag_sequence_realrooted_auto failed on the constant case
a n = 1, c n = 2. Its final normalized fallback expected
P(n+2) = P(n+1) + X * P(n). Replacing it with
rr_prec_pos_X_lag_sequence_realrooted and explicit proofs of 0 < 1 and
0 <= 2 builds successfully. The current main source has the same auto
expansion.

Suggested scope:

• make the auto frontend infer non-unit constant or n-dependent scalar lag
  coefficients when the recurrence is already in explicit C(a n) / C(c n)
  form, or expose a small auto variant that accepts the coefficient functions
  while discharging their sign goals automatically;
• preserve the existing unit-lag fallback;
• add executable examples for c n = 2 and a simple nonconstant nonnegative
  c n.

Immediate affected families include A128099 and likely the queued A059344
transfer. This is an automation/frontend gap, not a missing real-rootedness
theorem.