# Example: Commutativity of Multiplication

The commutativity of multiplication means that the following equation holds

`m * n = n * m`

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

```//
prfun
mul_commute{m,n:int}{p:int}(MUL(m, n, p)): MUL(n, m, p)
//
```

An implementation of mul_commute is given as follows:

```primplmnt
mul_commute
{m,n}{p}(pf0) = let
//
prfun
auxnat
{m:nat}
{p:int} .<m>.
(
pf: MUL(m, n, p)
) : MUL(n, m, p) =
(
case+ pf of
| MULbas() => mul_nx0_0{n}()
| MULind(pf1) =>
mul_distribute(auxnat(pf1), mul_nx1_n{n}())
// end of [MULind]
) (* end of [auxnat] *)
//
in
//
sif
m >= 0
then auxnat(pf0)
else let
prval MULneg(pf1) = pf0 in mul_neg_2(auxnat(pf1))
end // end of [else]
//
end // end of [mul_commute]
```

where the following proof functions are called:

```//
prfun
mul_nx0_0{n:int}(): MUL(n, 0, 0) // n * 0 = 0
//
prfun
mul_nx1_n{n:int}(): MUL(n, 1, n) // n * 1 = n
//
prfun
mul_neg_2
{m,n:int}{p:int}(MUL(m,n,p)): MUL(m,~n,~p) // m*(~n) = ~(m*n)
//
```

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

`m * n = n * m`

for m ranging over natural numbers and n ranging over integers. The function mul_commute can then be implemented immediately based on auxnat.