The general FormulaGenerator maps nrt operations to sqrtint or sqrtnint functions. Extend the LEAN formula generator to also support such programs/functions. Figure out whether LEAN has native support for it, or if there are modules for this, or if we can add ad-hoc function definitions to the generated code.