For t>=1, (t+1)!>=2^t; for r>=1,m>=1, (mr)!>=r! * r^((m-1)r). All quotient formulations are derived by positive clearing.
Method: native-induction. Induction: t and factorial-product length. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.