sig
  type t = Z.t Monome.monome
  val const : Z.t -> Monome.Int.t
  val singleton : Z.t -> Monome.term -> Monome.Int.t
  val of_list : Z.t -> (Z.t * Monome.term) list -> Monome.Int.t
  val of_term : Monome.term -> Monome.Int.t option
  val of_term_exn : Monome.term -> Monome.Int.t
  val to_term : Monome.Int.t -> Monome.term
  val normalize : Monome.Int.t -> Monome.Int.t
  val has_instances : Monome.Int.t -> bool
  val quotient : Monome.Int.t -> Z.t -> Monome.Int.t option
  val divisible : Monome.Int.t -> Z.t -> bool
  val factorize : Monome.Int.t -> (Monome.Int.t * Z.t) option
  val normalize_wrt_zero : Monome.Int.t -> Monome.Int.t
  val reduce_same_factor :
    Monome.Int.t ->
    Monome.Int.t -> Monome.term -> Monome.Int.t * Monome.Int.t
  val compare :
    (Monome.term -> Monome.term -> Libzipperposition.Comparison.t) ->
    Monome.Int.t -> Monome.Int.t -> Libzipperposition.Comparison.t
  val to_multiset : Monome.Int.t -> Multisets.MT.t
  module Modulo :
    sig
      val modulo : n:Z.t -> Z.t -> Z.t
      val sum : n:Z.t -> Z.t -> Z.t -> Z.t
      val uminus : n:Z.t -> Z.t -> Z.t
    end
  module Solve :
    sig
      type solution = (Monome.term * Monome.Int.t) list
      val split_solution :
        Monome.Int.Solve.solution ->
        Libzipperposition.Substs.t * Monome.Int.Solve.solution
      val diophant2 : Z.t -> Z.t -> Z.t -> Z.t * Z.t * Z.t
      val diophant_l : Z.t list -> Z.t -> Z.t list * Z.t
      val coeffs_n : Z.t list -> Z.t -> Monome.term list -> Monome.Int.t list
      val eq_zero :
        ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
        Monome.Int.t -> Monome.Int.Solve.solution list
      val lower_zero :
        ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
        strict:bool -> Monome.Int.t -> Monome.Int.Solve.solution list
      val lt_zero :
        ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
        Monome.Int.t -> Monome.Int.Solve.solution list
      val leq_zero :
        ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
        Monome.Int.t -> Monome.Int.Solve.solution list
      val neq_zero :
        ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
        Monome.Int.t -> Monome.Int.Solve.solution list
    end
end