La funzione binomiale, chiamata BinCoeff nel seguito, è definita sull’insieme delle coppie di numeri naturali e fornisce risultati detti numeri binomiali:
In particolare, il numero binomiale indicato come (n k) denota il numero di differenti modi di scegliere un sottoinsieme di k elementi da un insieme di n elementi. Come è ben noto, i numeri binomiali possono essere disposti a formare un matrice triangolare, detta triangolo di Pascal,1 come illustrato dalla Tavola 1. Una formula standard per il calcolo dei numeri binomiali è
 | (1) |
| DEF BinCoeff0 (n,k::IsNat) = |