The generic FormulaGenerator converts bin operations to binomial functions. Extend the LEAN formula generator to support this as well. We'll need to find out if LEAN natively supports binomila coeeficients, or if there are modules for it, or if we need to add ad-hoc (recursive) functions for it.