Support binomial in LEAN formula generation

[ckrause]

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.

[ckrause]

For non-negative arguments (Nat), we could use Nat.choose. But then we would need to integrate a range check to find out if it is non-negative.