The commutativity of multiplication means that the following equation holds
for m and n ranging over integers. A direct encoding of this equation is given by the following (proof) function interface: 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]