let rec divide a (y, n) =
  let ((y', m), post) = decompose a in
  let cmp = Term.cmp y y' in
    if cmp < 0 then       (* [y << y'] *)
      (match post with
         | Some(b') -> mk_mult (mk_expt y' m) (divide b' (y, n))
         | None -> invalid_arg "Pprod.divide: denumerator not found")
    else if cmp = 0 then 
      (match post with
         | Some(b') -> 
             assert(n <= m);
             mk_mult (mk_expt y' (m - n)) b'
         | None -> 
             mk_expt y' (m - n))
    else    
      invalid_arg "Pprod.divide: denumerator not found"