let rec mk_expt a n = assert(n >= 0); if n = 0 then Arith.mk_one() else mk_mult a (mk_expt a (n - 1))