let rec mk_mult a b =
  if Term.eq a b then        (* [ a * a --> a^2] *)
    mk_expt 2 a
  else if Pp.is_one a then
    b
  else if Pp.is_one b then
    a
  else 
    match a, b with
      | App(Arith(op), xl), _ ->
          mk_mult_arith op xl b
      | _, App(Arith(op), yl) ->
          mk_mult_arith op yl a
      | _ ->
          mk_inj (Pp.mk_mult a b)

and mk_inj pp =
  if Pp.is_one pp then
    Arith.mk_one
  else 
    pp
           

and mk_mult_arith op yl b =
  match op, yl with
    | Num(q), [] -> 
        Arith.mk_multq q b
    | Multq(q), [x] -> 
        if Pp.is_one x then
          Arith.mk_multq q b
        else 
          Arith.mk_multq q (mk_mult x b)
    | Add, _ ->
        mk_mult_add b yl
    | _ ->
        assert false

and mk_mult_add a yl =
  Arith.mk_addl (mapl (mk_mult a) yl)


and mk_multl al =
  List.fold_left mk_mult Arith.mk_one al


and mk_expt n a =
  if n = 0 then 
    Arith.mk_one
  else if n = 1 then
    a
  else match a with
    | App(Arith(op), xl) ->
        mk_expt_arith n op xl
    | _ ->
        mk_inj (Pp.mk_expt n a)

and mk_expt_arith n op xl =
  match op, xl with
    | Num(q), [] ->                       (* case [q^n] *)
        if n >= 0 then
          Arith.mk_num (Mpa.Q.expt q n)
        else if n = -1 && not(Q.is_zero q) then
          Arith.mk_num (Mpa.Q.inv q)
        else 
          mk_inj (Pp.mk_expt (-1) (Arith.mk_num q))
    | Multq(q), [x] ->                    (* [(q * x)^n = q^n * x^n] *)
        if n >= 0 then
          Arith.mk_multq (Mpa.Q.expt q n) (mk_expt n x)
        else if n = -1 && not(Q.is_zero q) then
          Arith.mk_multq (Mpa.Q.inv q) (mk_inj (Pp.mk_expt (-1)  x))
        else 
          mk_inj (Pp.mk_expt n (Pp.mk_mult (Arith.mk_num q) x))
    | Add, _ ->                           (* case [(x1 + ... + xk)^n]  *)
        mk_expt_add n xl 
    | _ ->
        assert false

and mk_expt_add n xl =
  if n = 0 then
    Arith.mk_one
  else if n = 1 then 
    Arith.mk_addl xl
  else if n > 1 then
    mk_mult_add (mk_expt_add (n - 1) xl) xl
  else
    mk_inj (Pp.mk_expt n (Arith.mk_addl xl))