IR053 — Factorial-binomial cancellation

binomial(N+s,s)/(N+s)!=1/(N!*s!); derive by positive integer factorial identities.

Method: native-induction. Induction: s. Risk: routine.

This is a human-readable planning contract, not a parsed kernel formula or accepted proof.

Planned prerequisites and notation

• IR011 — Factorial lower bounds
• IR005 — Finite rational folds