# Example: Distributivity of Multiplication

The distributivity of multiplication over addition means that the following equation holds

`m * (n1 + n2) = m * n1 + m * n2`

for m, n1 and n2 ranging over integers. A direct encoding of the equation is given by the following (proof) function interface:

```//
prfun
mul_distribute
{m,n1,n2:int}{p1,p2:int}
(MUL(m, n1, p1), MUL(m, n2, p2)): MUL(m, n1+n2, p1+p2)
//
```

Plainly speaking, the encoding states that the product of m and (n1+n2) is p1+p2 if the product of m and n1 is p1 and the product of m and n2 is p2. An implementation of mul_distribute is given as follows:

```primplement
mul_distribute
{m,n1,n2}{p1,p2}
(pf1, pf2) = let
//
prfun
auxnat
{m:nat}{p1,p2:int} .<m>.
(
pf1: MUL(m, n1, p1), pf2: MUL(m, n2, p2)
) : MUL(m, n1+n2, p1+p2) =
(
case+ (pf1, pf2) of
| (MULbas(), MULbas()) => MULbas()
| (MULind pf1, MULind pf2) => MULind(auxnat (pf1, pf2))
) (* end of [auxnat] *)
//
in
//
sif
m >= 0
then (
auxnat (pf1, pf2)
) // end of [then]
else let
prval MULneg(pf1) = pf1
prval MULneg(pf2) = pf2
in
MULneg(auxnat (pf1, pf2))
end // end of [else]
//
end // end of [mul_distribute]
```

The inner function auxnat encodes a straighforward proof based on mathematical induction that establishes the following equation:

```m * (n1 + n2) = m * n1 + m * n2
```

for m ranging over natural numbers and n1 and n2 ranging over integers. The function mul_distribute can then be implemented immediately based on auxnat.