let rec mk_multq q a =
  let rec multq q = function
    | [] -> []
    | m :: ml ->
        let (p,x) = mono_of m in
          (of_mono (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, ml) = poly_of a in
        of_poly (Q.mult q p) (multq q ml)

and mk_addq q a =
  if Q.is_zero q then a else
    match a with
      | App(Arith(Num(p)), []) ->
          mk_num (Q.add q p)
      | App(Arith(Multq(_)), [_]) ->
          mk_app add [mk_num q; a]
      | App(Arith(Add), xl) ->
          (match xl with
             | App(Arith(Num(p)), []) :: xl' ->
                 let q_plus_p = Q.add q p in
                   if Q.is_zero q_plus_p then
                     mk_app add xl'
                   else 
                     mk_app add (mk_num q_plus_p :: xl')
             | _ -> 
                 mk_app add (mk_num q :: xl))
      | _ ->
          mk_app 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, x1) =  mono_of m1 in
          let (q2, x2) = mono_of 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 
                  (of_mono q x1) :: (map2 l1' l2')
            else if cmp < 0 then
              m2 :: map2 l1 l2'
          else (* cmp > 0 *)
            m1 :: map2 l1' l2
  in
  let (q, l) = poly_of a in
  let (p, m) = poly_of b in
    of_poly (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 :: xl -> mk_add x (mk_addl xl)
 
and mk_incr a =
  let (q, l) = poly_of a in
  of_poly (Q.add 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)