let div (pp, qq) =
try
let rec loop acc al bl =
match al, bl with
| [], [] ->
acc
| [], bl ->
mk_mult acc (mk_multl bl)
| al, [] ->
raise Not_found
| a :: al', b :: bl' ->
let (x, n) = destruct a
and (y, m) = destruct b in
let cmp = Term.cmp x y in
if cmp = 0 then
if n = m then
loop acc al' bl'
else if n < m then
loop (mk_mult acc (mk_expt (m - n) x)) al' bl'
else
raise Not_found
else if cmp > 0 then
loop (mk_mult b acc) al bl'
else
raise Not_found
in
Some(loop mk_one (to_list pp) (to_list qq))
with
Not_found -> None