let rec mk_multq q a =
  let rec multq q = function
    | [] -> 
        []
    | m :: ml ->
        let p = coefficient_of_mono m
        and x = variable_of_mono m in
          (mk_monomial (Q.mult q p) x) :: (multq q ml)
  in
    if Q.is_zero q then 
      mk_zero()
    else if Q.is_one q then 
      a
    else 
      let p = constant_of a
      and ml = nonconstant_monomials_of a in
        mk_polynomial (Q.mult q p) (multq q ml)

and mk_addq q a =
  let add = Term.App.mk_app Sym.Arith.mk_add in
  if Q.is_zero q then a else
    match a with
      | Term.App((Sym.Arith(op), _), al, _) ->
          (match op, al with
             | Sym.Num(p), [] ->
                 mk_num (Q.add q p)
             | Sym.Multq(_), [_] ->
                 add [mk_num q; a]
             | Sym.Add, [] ->
                 mk_num q
             | Sym.Add, ((x :: xl') as xl) ->
                 (try
                    let p = d_num x in
                    let q_plus_p = Q.add q p in
                      if Q.is_zero q_plus_p then
                        add xl'
                      else 
                        add (mk_num q_plus_p :: xl')
                  with
                      Not_found -> add (mk_num q :: xl))
             | _ ->
                 assert false)
      | _ -> 
          add [mk_num q; a]

and mk_add a b =
  let rec map2 l1 l2 =      (* Add two polynomials *)
    match l1, l2 with
      | [], _ -> l2
      | _ , [] -> l1
      | m1 :: l1', m2 :: l2' ->
          let q1 = coefficient_of_mono m1
          and x1 = variable_of_mono m1
          and q2 = coefficient_of_mono m2
          and x2 = variable_of_mono m2 in
          let cmp = Term.cmp x1 x2 in
            if cmp = 0 then
              let q = Q.add q1 q2 in
                if Q.is_zero q then 
                  map2 l1' l2'
                else 
                  (mk_monomial q x1) :: (map2 l1' l2')
            else if cmp < 0 then
              m2 :: map2 l1 l2'
            else (* cmp > 0 *)
              m1 :: map2 l1' l2
  in
  let q = constant_of a
  and l = nonconstant_monomials_of a
  and p = constant_of b
  and m = nonconstant_monomials_of b in
    mk_polynomial (Q.add q p) (map2 l m) 

and mk_addl l =
  match l with
    | [] -> mk_zero()
    | [x] -> x
    | [x; y] -> mk_add x y
    | [x; y; z] -> mk_add x (mk_add y z)
    | x :: xl -> mk_add x (mk_addl xl)
 
and mk_incr a =
  let q = constant_of a
  and l = nonconstant_monomials_of a in
    mk_polynomial (Q.add q Q.one) l

and mk_decr a =
  let q = constant_of a
  and l = nonconstant_monomials_of a in
    mk_polynomial (Q.sub q Q.one) l

and mk_neg a =
  mk_multq (Q.minus (Q.one)) a

and mk_sub a b =
  mk_add a (mk_neg b)