With n<=r and q²=28n, prove r!/(7r)!<=r^(-6r) and q^(8r)<=28^(4r)*r^(4r), by cleared positive inequalities.
Method: native-order. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.