let leading_coef =
  let rec
    f = function
      p -> (* not (is_null_poly (p)) *)
           let
             (a, q) = inv_cons_poly (p)
           in
             if is_null_poly (q)
               then a
               else f (q)
  in
    function
      p -> if not (is_null_poly (p))
             then f (p)
             else failwith ("leading_coef : requires a non-null polynomial as its argument")