let euclid_div_poly =
  let rec
    f = function
      p1, p2 -> (* not (is_null_poly (p2)) *)
                if is_null_poly (p1)
                  then (null_poly (), null_poly ())
                  else
                    let
                      d1 = degree (p1)
                      and
                      d2 = degree (p2)
                    in
                      if d1 < d2
                        then (null_poly (), p1)
                        else
                          let
                            a1 = leading_coef (p1)
                            and
                            a2 = leading_coef (p2)
                          in
                            (* not (eq_rat (a1, cons_rat (", "))) 
                               & not (eq_rat (a2, cons_rat (", "))) *)
                            let
                              a = div_rat (a1, a2)
                            in
                              (* not (eq_rat (a, cons_rat (", "))) & d1 - d2 >= 0 *)
                              let
                                m = monomial (a, d1 - d2)
                              in
                                let
                                  p = mult_poly (rat_times_poly (cons_rat ("-1", "1"), m), p2)
                                in
                                  let
                                    p1_1 = add_poly (p1, p)
                                  in
                                    let
                                      (q, r) = f (p1_1, p2)
                                    in
                                      (add_poly (m, q), r)
                                      
  in
    function
      p1, p2 -> if not (is_null_poly (p2))
                  then f (p1, p2)
                  else failwith ("euclid_div_poly : requires a non-null polynomial as its second argument")